; benchmark generated from python API
(set-info :status unknown)
(declare-fun icon2_feasible () Bool)
(declare-fun tbl4_kid_7_kid_2_feasible () Bool)
(declare-fun tbl4_kid_7_feasible () Bool)
(declare-fun tbl4_kid_7_kid_1_feasible () Bool)
(declare-fun tbl4_kid_7_kid_0_feasible () Bool)
(declare-fun tbl4_kid_6_kid_2_feasible () Bool)
(declare-fun tbl4_kid_6_feasible () Bool)
(declare-fun tbl4_kid_6_kid_1_feasible () Bool)
(declare-fun tbl4_kid_6_kid_0_feasible () Bool)
(declare-fun tbl4_kid_5_kid_2_feasible () Bool)
(declare-fun tbl4_kid_5_feasible () Bool)
(declare-fun tbl4_kid_5_kid_1_feasible () Bool)
(declare-fun tbl4_kid_5_kid_0_feasible () Bool)
(declare-fun tbl4_kid_4_kid_2_feasible () Bool)
(declare-fun tbl4_kid_4_feasible () Bool)
(declare-fun tbl4_kid_4_kid_1_feasible () Bool)
(declare-fun tbl4_kid_4_kid_0_feasible () Bool)
(declare-fun tbl4_kid_3_kid_2_feasible () Bool)
(declare-fun tbl4_kid_3_feasible () Bool)
(declare-fun tbl4_kid_3_kid_1_feasible () Bool)
(declare-fun tbl4_kid_3_kid_0_feasible () Bool)
(declare-fun tbl4_kid_2_kid_2_feasible () Bool)
(declare-fun tbl4_kid_2_feasible () Bool)
(declare-fun tbl4_kid_2_kid_1_feasible () Bool)
(declare-fun tbl4_kid_2_kid_0_feasible () Bool)
(declare-fun tbl4_kid_1_kid_2_feasible () Bool)
(declare-fun tbl4_kid_1_feasible () Bool)
(declare-fun tbl4_kid_1_kid_1_feasible () Bool)
(declare-fun tbl4_kid_1_kid_0_feasible () Bool)
(declare-fun tbl4_kid_0_kid_2_feasible () Bool)
(declare-fun tbl4_kid_0_feasible () Bool)
(declare-fun tbl4_kid_0_kid_1_feasible () Bool)
(declare-fun tbl4_kid_0_kid_0_feasible () Bool)
(declare-fun tbl4_feasible () Bool)
(declare-fun tbl3_feasible () Bool)
(declare-fun tbl_holder_feasible () Bool)
(declare-fun shop_feasible () Bool)
(declare-fun alexa_feasible () Bool)
(declare-fun Basket_feasible () Bool)
(declare-fun Help_feasible () Bool)
(declare-fun your_account_feasible () Bool)
(declare-fun accounts_feasible () Bool)
(declare-fun search_go_feasible () Bool)
(declare-fun search_bar_feasible () Bool)
(declare-fun icon_feasible () Bool)
(declare-fun bottom_feasible () Bool)
(declare-fun main_body_feasible () Bool)
(declare-fun search_feasible () Bool)
(declare-fun back_ground_feasible () Bool)
(declare-fun icon2_hight () Real)
(declare-fun icon2_width () Real)
(declare-fun bottom_width () Real)
(declare-fun icon2_x () Real)
(declare-fun bottom_x () Real)
(declare-fun bottom_hight () Real)
(declare-fun icon2_y () Real)
(declare-fun bottom_y () Real)
(declare-fun back_ground_width () Real)
(declare-fun back_ground_x () Real)
(declare-fun tbl4_kid_0_width () Real)
(declare-fun tbl4_kid_2_width () Real)
(declare-fun tbl4_kid_1_width () Real)
(declare-fun tbl4_kid_3_hight () Real)
(declare-fun tbl4_kid_0_hight () Real)
(declare-fun tbl4_kid_0_y () Real)
(declare-fun tbl4_kid_3_y () Real)
(declare-fun tbl4_kid_2_x () Real)
(declare-fun tbl4_kid_1_x () Real)
(declare-fun tbl4_kid_0_x () Real)
(declare-fun tbl4_kid_5_width () Real)
(declare-fun tbl4_kid_5_x () Real)
(declare-fun tbl4_kid_4_width () Real)
(declare-fun tbl4_kid_4_x () Real)
(declare-fun tbl4_kid_3_width () Real)
(declare-fun tbl4_kid_3_x () Real)
(declare-fun tbl4_kid_5_hight () Real)
(declare-fun tbl4_kid_5_y () Real)
(declare-fun tbl4_kid_4_hight () Real)
(declare-fun tbl4_kid_4_y () Real)
(declare-fun tbl4_kid_2_hight () Real)
(declare-fun tbl4_kid_2_y () Real)
(declare-fun tbl4_kid_1_hight () Real)
(declare-fun tbl4_kid_1_y () Real)
(declare-fun tbl3_y () Real)
(declare-fun tbl3_hight () Real)
(declare-fun tbl3_width () Real)
(declare-fun tbl3_x () Real)
(declare-fun tbl4_kid_7_kid_2_hight () Real)
(declare-fun tbl4_kid_7_kid_0_hight () Real)
(declare-fun tbl4_kid_7_kid_1_hight () Real)
(declare-fun tbl4_kid_7_kid_1_y () Real)
(declare-fun tbl4_kid_7_kid_2_y () Real)
(declare-fun tbl4_kid_7_kid_0_y () Real)
(declare-fun tbl4_kid_7_y () Real)
(declare-fun tbl4_kid_7_hight () Real)
(declare-fun tbl4_kid_7_x () Real)
(declare-fun tbl4_kid_7_kid_2_width () Real)
(declare-fun tbl4_kid_7_kid_2_x () Real)
(declare-fun tbl4_kid_7_width () Real)
(declare-fun tbl4_kid_7_kid_1_width () Real)
(declare-fun tbl4_kid_7_kid_1_x () Real)
(declare-fun tbl4_kid_7_kid_0_x () Real)
(declare-fun tbl4_kid_7_kid_0_width () Real)
(declare-fun tbl4_kid_6_kid_2_hight () Real)
(declare-fun tbl4_kid_6_kid_0_hight () Real)
(declare-fun tbl4_kid_6_kid_1_hight () Real)
(declare-fun tbl4_kid_6_kid_1_y () Real)
(declare-fun tbl4_kid_6_kid_2_y () Real)
(declare-fun tbl4_kid_6_kid_0_y () Real)
(declare-fun tbl4_kid_6_y () Real)
(declare-fun tbl4_kid_6_hight () Real)
(declare-fun tbl4_kid_6_kid_2_x () Real)
(declare-fun tbl4_kid_6_width () Real)
(declare-fun tbl4_kid_6_x () Real)
(declare-fun tbl4_kid_6_kid_2_width () Real)
(declare-fun tbl4_kid_6_kid_1_width () Real)
(declare-fun tbl4_kid_6_kid_1_x () Real)
(declare-fun tbl4_kid_6_kid_0_width () Real)
(declare-fun tbl4_kid_6_kid_0_x () Real)
(declare-fun tbl4_kid_5_kid_2_hight () Real)
(declare-fun tbl4_kid_5_kid_0_hight () Real)
(declare-fun tbl4_kid_5_kid_2_y () Real)
(declare-fun tbl4_kid_5_kid_1_hight () Real)
(declare-fun tbl4_kid_5_kid_1_y () Real)
(declare-fun tbl4_kid_5_kid_0_y () Real)
(declare-fun tbl4_kid_5_kid_2_width () Real)
(declare-fun tbl4_kid_5_kid_2_x () Real)
(declare-fun tbl4_kid_5_kid_1_width () Real)
(declare-fun tbl4_kid_5_kid_1_x () Real)
(declare-fun tbl4_kid_5_kid_0_width () Real)
(declare-fun tbl4_kid_5_kid_0_x () Real)
(declare-fun tbl4_kid_4_kid_2_hight () Real)
(declare-fun tbl4_kid_4_kid_0_hight () Real)
(declare-fun tbl4_kid_4_kid_1_hight () Real)
(declare-fun tbl4_kid_4_kid_2_y () Real)
(declare-fun tbl4_kid_4_kid_1_y () Real)
(declare-fun tbl4_kid_4_kid_0_y () Real)
(declare-fun tbl4_kid_4_kid_2_x () Real)
(declare-fun tbl4_kid_4_kid_2_width () Real)
(declare-fun tbl4_kid_4_kid_1_x () Real)
(declare-fun tbl4_kid_4_kid_1_width () Real)
(declare-fun tbl4_kid_4_kid_0_width () Real)
(declare-fun tbl4_kid_4_kid_0_x () Real)
(declare-fun tbl4_kid_3_kid_2_hight () Real)
(declare-fun tbl4_kid_3_kid_0_hight () Real)
(declare-fun tbl4_kid_3_kid_2_y () Real)
(declare-fun tbl4_kid_3_kid_1_hight () Real)
(declare-fun tbl4_kid_3_kid_1_y () Real)
(declare-fun tbl4_kid_3_kid_0_y () Real)
(declare-fun tbl4_kid_3_kid_2_width () Real)
(declare-fun tbl4_kid_3_kid_2_x () Real)
(declare-fun tbl4_kid_3_kid_1_width () Real)
(declare-fun tbl4_kid_3_kid_1_x () Real)
(declare-fun tbl4_kid_3_kid_0_width () Real)
(declare-fun tbl4_kid_3_kid_0_x () Real)
(declare-fun tbl4_kid_2_kid_2_hight () Real)
(declare-fun tbl4_kid_2_kid_0_hight () Real)
(declare-fun tbl4_kid_2_kid_1_hight () Real)
(declare-fun tbl4_kid_2_kid_1_y () Real)
(declare-fun tbl4_kid_2_kid_2_y () Real)
(declare-fun tbl4_kid_2_kid_0_y () Real)
(declare-fun tbl4_kid_2_kid_2_x () Real)
(declare-fun tbl4_kid_2_kid_2_width () Real)
(declare-fun tbl4_kid_2_kid_1_x () Real)
(declare-fun tbl4_kid_2_kid_1_width () Real)
(declare-fun tbl4_kid_2_kid_0_x () Real)
(declare-fun tbl4_kid_2_kid_0_width () Real)
(declare-fun tbl4_kid_1_kid_2_hight () Real)
(declare-fun tbl4_kid_1_kid_0_hight () Real)
(declare-fun tbl4_kid_1_kid_2_y () Real)
(declare-fun tbl4_kid_1_kid_1_hight () Real)
(declare-fun tbl4_kid_1_kid_1_y () Real)
(declare-fun tbl4_kid_1_kid_0_y () Real)
(declare-fun tbl4_kid_1_kid_2_width () Real)
(declare-fun tbl4_kid_1_kid_2_x () Real)
(declare-fun tbl4_kid_1_kid_1_width () Real)
(declare-fun tbl4_kid_1_kid_1_x () Real)
(declare-fun tbl4_kid_1_kid_0_width () Real)
(declare-fun tbl4_kid_1_kid_0_x () Real)
(declare-fun tbl4_kid_0_kid_2_hight () Real)
(declare-fun tbl4_kid_0_kid_0_hight () Real)
(declare-fun tbl4_kid_0_kid_1_hight () Real)
(declare-fun tbl4_kid_0_kid_1_y () Real)
(declare-fun tbl4_kid_0_kid_2_y () Real)
(declare-fun tbl4_kid_0_kid_0_y () Real)
(declare-fun tbl4_kid_0_kid_2_width () Real)
(declare-fun tbl4_kid_0_kid_2_x () Real)
(declare-fun tbl4_kid_0_kid_1_width () Real)
(declare-fun tbl4_kid_0_kid_1_x () Real)
(declare-fun tbl4_kid_0_kid_0_x () Real)
(declare-fun tbl4_kid_0_kid_0_width () Real)
(declare-fun tbl4_hight () Real)
(declare-fun tbl4_y () Real)
(declare-fun tbl4_width () Real)
(declare-fun tbl4_x () Real)
(declare-fun tbl_holder_width () Real)
(declare-fun tbl_holder_x () Real)
(declare-fun main_body_width () Real)
(declare-fun main_body_x () Real)
(declare-fun tbl_holder_hight () Real)
(declare-fun tbl_holder_y () Real)
(declare-fun shop_width () Real)
(declare-fun shop_x () Real)
(declare-fun shop_hight () Real)
(declare-fun main_body_y () Real)
(declare-fun alexa_y () Real)
(declare-fun alexa_x () Real)
(declare-fun alexa_width () Real)
(declare-fun alexa_hight () Real)
(declare-fun shop_y () Real)
(declare-fun main_body_hight () Real)
(declare-fun search_go_width () Real)
(declare-fun search_go_x () Real)
(declare-fun accounts_x () Real)
(declare-fun search_bar_width () Real)
(declare-fun search_bar_x () Real)
(declare-fun icon_x () Real)
(declare-fun icon_width () Real)
(declare-fun your_account_width () Real)
(declare-fun Basket_width () Real)
(declare-fun Help_width () Real)
(declare-fun Basket_x () Real)
(declare-fun Help_x () Real)
(declare-fun your_account_x () Real)
(declare-fun Basket_hight () Real)
(declare-fun Basket_y () Real)
(declare-fun accounts_hight () Real)
(declare-fun accounts_y () Real)
(declare-fun Help_y () Real)
(declare-fun Help_hight () Real)
(declare-fun your_account_y () Real)
(declare-fun your_account_hight () Real)
(declare-fun accounts_width () Real)
(declare-fun search_hight () Real)
(declare-fun search_y () Real)
(declare-fun search_go_hight () Real)
(declare-fun search_go_y () Real)
(declare-fun search_bar_hight () Real)
(declare-fun search_bar_y () Real)
(declare-fun icon_hight () Real)
(declare-fun icon_y () Real)
(declare-fun search_width () Real)
(declare-fun search_x () Real)
(declare-fun BC_x () Real)
(declare-fun BC_width () Real)
(declare-fun back_ground_hight () Real)
(declare-fun back_ground_y () Real)
(declare-fun BC_feasible () Bool)
(declare-fun BC_y () Real)
(declare-fun BC_hight () Real)
(assert
 (let (($x1617 (not tbl4_kid_7_feasible)))
 (let (($x1896 (or $x1617 tbl4_kid_7_kid_2_feasible)))
 (let (($x1894 (not tbl4_kid_7_kid_2_feasible)))
 (let (($x1895 (or $x1894 tbl4_kid_7_feasible)))
 (let (($x1893 (or $x1617 tbl4_kid_7_kid_1_feasible)))
 (let (($x1891 (not tbl4_kid_7_kid_1_feasible)))
 (let (($x1892 (or $x1891 tbl4_kid_7_feasible)))
 (let (($x1890 (or $x1617 tbl4_kid_7_kid_0_feasible)))
 (let (($x1888 (not tbl4_kid_7_kid_0_feasible)))
 (let (($x1889 (or $x1888 tbl4_kid_7_feasible)))
 (let (($x1509 (not tbl4_kid_6_feasible)))
 (let (($x1887 (or $x1509 tbl4_kid_6_kid_2_feasible)))
 (let (($x1885 (not tbl4_kid_6_kid_2_feasible)))
 (let (($x1886 (or $x1885 tbl4_kid_6_feasible)))
 (let (($x1884 (or $x1509 tbl4_kid_6_kid_1_feasible)))
 (let (($x1882 (not tbl4_kid_6_kid_1_feasible)))
 (let (($x1883 (or $x1882 tbl4_kid_6_feasible)))
 (let (($x1881 (or $x1509 tbl4_kid_6_kid_0_feasible)))
 (let (($x1879 (not tbl4_kid_6_kid_0_feasible)))
 (let (($x1880 (or $x1879 tbl4_kid_6_feasible)))
 (let (($x1403 (not tbl4_kid_5_feasible)))
 (let (($x1878 (or $x1403 tbl4_kid_5_kid_2_feasible)))
 (let (($x1876 (not tbl4_kid_5_kid_2_feasible)))
 (let (($x1877 (or $x1876 tbl4_kid_5_feasible)))
 (let (($x1875 (or $x1403 tbl4_kid_5_kid_1_feasible)))
 (let (($x1873 (not tbl4_kid_5_kid_1_feasible)))
 (let (($x1874 (or $x1873 tbl4_kid_5_feasible)))
 (let (($x1872 (or $x1403 tbl4_kid_5_kid_0_feasible)))
 (let (($x1870 (not tbl4_kid_5_kid_0_feasible)))
 (let (($x1871 (or $x1870 tbl4_kid_5_feasible)))
 (let (($x1293 (not tbl4_kid_4_feasible)))
 (let (($x1869 (or $x1293 tbl4_kid_4_kid_2_feasible)))
 (let (($x1867 (not tbl4_kid_4_kid_2_feasible)))
 (let (($x1868 (or $x1867 tbl4_kid_4_feasible)))
 (let (($x1866 (or $x1293 tbl4_kid_4_kid_1_feasible)))
 (let (($x1864 (not tbl4_kid_4_kid_1_feasible)))
 (let (($x1865 (or $x1864 tbl4_kid_4_feasible)))
 (let (($x1863 (or $x1293 tbl4_kid_4_kid_0_feasible)))
 (let (($x1861 (not tbl4_kid_4_kid_0_feasible)))
 (let (($x1862 (or $x1861 tbl4_kid_4_feasible)))
 (let (($x1183 (not tbl4_kid_3_feasible)))
 (let (($x1860 (or $x1183 tbl4_kid_3_kid_2_feasible)))
 (let (($x1858 (not tbl4_kid_3_kid_2_feasible)))
 (let (($x1859 (or $x1858 tbl4_kid_3_feasible)))
 (let (($x1857 (or $x1183 tbl4_kid_3_kid_1_feasible)))
 (let (($x1855 (not tbl4_kid_3_kid_1_feasible)))
 (let (($x1856 (or $x1855 tbl4_kid_3_feasible)))
 (let (($x1854 (or $x1183 tbl4_kid_3_kid_0_feasible)))
 (let (($x1852 (not tbl4_kid_3_kid_0_feasible)))
 (let (($x1853 (or $x1852 tbl4_kid_3_feasible)))
 (let (($x1074 (not tbl4_kid_2_feasible)))
 (let (($x1851 (or $x1074 tbl4_kid_2_kid_2_feasible)))
 (let (($x1849 (not tbl4_kid_2_kid_2_feasible)))
 (let (($x1850 (or $x1849 tbl4_kid_2_feasible)))
 (let (($x1848 (or $x1074 tbl4_kid_2_kid_1_feasible)))
 (let (($x1846 (not tbl4_kid_2_kid_1_feasible)))
 (let (($x1847 (or $x1846 tbl4_kid_2_feasible)))
 (let (($x1845 (or $x1074 tbl4_kid_2_kid_0_feasible)))
 (let (($x1843 (not tbl4_kid_2_kid_0_feasible)))
 (let (($x1844 (or $x1843 tbl4_kid_2_feasible)))
 (let (($x967 (not tbl4_kid_1_feasible)))
 (let (($x1842 (or $x967 tbl4_kid_1_kid_2_feasible)))
 (let (($x1840 (not tbl4_kid_1_kid_2_feasible)))
 (let (($x1841 (or $x1840 tbl4_kid_1_feasible)))
 (let (($x1839 (or $x967 tbl4_kid_1_kid_1_feasible)))
 (let (($x1837 (not tbl4_kid_1_kid_1_feasible)))
 (let (($x1838 (or $x1837 tbl4_kid_1_feasible)))
 (let (($x1836 (or $x967 tbl4_kid_1_kid_0_feasible)))
 (let (($x1834 (not tbl4_kid_1_kid_0_feasible)))
 (let (($x1835 (or $x1834 tbl4_kid_1_feasible)))
 (let (($x858 (not tbl4_kid_0_feasible)))
 (let (($x1833 (or $x858 tbl4_kid_0_kid_2_feasible)))
 (let (($x1831 (not tbl4_kid_0_kid_2_feasible)))
 (let (($x1832 (or $x1831 tbl4_kid_0_feasible)))
 (let (($x1830 (or $x858 tbl4_kid_0_kid_1_feasible)))
 (let (($x1828 (not tbl4_kid_0_kid_1_feasible)))
 (let (($x1829 (or $x1828 tbl4_kid_0_feasible)))
 (let (($x1827 (or $x858 tbl4_kid_0_kid_0_feasible)))
 (let (($x1825 (not tbl4_kid_0_kid_0_feasible)))
 (let (($x1826 (or $x1825 tbl4_kid_0_feasible)))
 (let (($x652 (not tbl4_feasible)))
 (let (($x1824 (or $x652 tbl4_kid_7_feasible)))
 (let (($x1823 (or $x1617 tbl4_feasible)))
 (let (($x1822 (or $x652 tbl4_kid_6_feasible)))
 (let (($x1821 (or $x1509 tbl4_feasible)))
 (let (($x667 (not tbl3_feasible)))
 (let (($x1820 (or $x652 $x667 $x1403)))
 (let (($x1819 (or tbl4_feasible tbl3_feasible $x1403)))
 (let (($x1818 (or $x667 tbl4_kid_5_feasible)))
 (let (($x1817 (or $x652 tbl4_kid_5_feasible)))
 (let (($x1816 (or $x652 $x667 $x1293)))
 (let (($x1815 (or tbl4_feasible tbl3_feasible $x1293)))
 (let (($x1814 (or $x667 tbl4_kid_4_feasible)))
 (let (($x1813 (or $x652 tbl4_kid_4_feasible)))
 (let (($x1812 (or $x652 $x667 $x1183)))
 (let (($x1811 (or tbl4_feasible tbl3_feasible $x1183)))
 (let (($x1810 (or $x667 tbl4_kid_3_feasible)))
 (let (($x1809 (or $x652 tbl4_kid_3_feasible)))
 (let (($x1808 (or $x652 $x667 $x1074)))
 (let (($x1807 (or tbl4_feasible tbl3_feasible $x1074)))
 (let (($x1806 (or $x667 tbl4_kid_2_feasible)))
 (let (($x1805 (or $x652 tbl4_kid_2_feasible)))
 (let (($x1804 (or $x652 $x667 $x967)))
 (let (($x1803 (or tbl4_feasible tbl3_feasible $x967)))
 (let (($x1802 (or $x667 tbl4_kid_1_feasible)))
 (let (($x1801 (or $x652 tbl4_kid_1_feasible)))
 (let (($x1800 (or $x652 $x667 $x858)))
 (let (($x1799 (or tbl4_feasible tbl3_feasible $x858)))
 (let (($x1798 (or $x667 tbl4_kid_0_feasible)))
 (let (($x1797 (or $x652 tbl4_kid_0_feasible)))
 (let (($x1796 (= (+ (- 50.0) icon2_hight) 0.0)))
 (let (($x1794 (= (+ (- 100.0) icon2_width) 0.0)))
 (let ((?x1791 (+ (- (+ (* (- 2.0) bottom_x) (* 2.0 icon2_x)) bottom_width) icon2_width)))
 (let (($x1792 (= ?x1791 0.0)))
 (let ((?x1785 (- (+ (- icon2_hight (* 2.0 bottom_y)) (* 2.0 icon2_y)) bottom_hight)))
 (let (($x1786 (= ?x1785 0.0)))
 (let (($x1780 (>= icon2_hight 0.0)))
 (let (($x1779 (>= icon2_width 0.0)))
 (let (($x1778 (>= icon2_y 0.0)))
 (let (($x1777 (>= icon2_x 0.0)))
 (let (($x1776 (= (+ (- 100.0) bottom_hight) 0.0)))
 (let (($x1774 (= (- (- (+ bottom_x bottom_width) back_ground_x) back_ground_width) 0.0)))
 (let ((?x307 (- bottom_x back_ground_x)))
 (let (($x1770 (= ?x307 0.0)))
 (let (($x841 (= (+ (- tbl4_kid_2_width) tbl4_kid_0_width) 0.0)))
 (let (($x1769 (or $x667 $x841)))
 (let (($x837 (= (+ (- tbl4_kid_1_width) tbl4_kid_0_width) 0.0)))
 (let (($x1768 (or $x667 $x837)))
 (let (($x762 (= (- tbl4_kid_0_hight tbl4_kid_3_hight) 0.0)))
 (let (($x1767 (or $x667 $x762)))
 (let (($x1765 (= (- (+ (- (- 10.0) tbl4_kid_0_hight) tbl4_kid_3_y) tbl4_kid_0_y) 0.0)))
 (let (($x1766 (or $x667 $x1765)))
 (let (($x820 (= (+ (- (- (- 10.0) tbl4_kid_1_x) tbl4_kid_1_width) tbl4_kid_2_x) 0.0)))
 (let (($x1762 (or $x667 $x820)))
 (let (($x815 (= (- (+ (- (- 10.0) tbl4_kid_0_x) tbl4_kid_1_x) tbl4_kid_0_width) 0.0)))
 (let (($x1761 (or $x667 $x815)))
 (let (($x1760 (or $x667 (= (- tbl4_kid_2_width tbl4_kid_5_width) 0.0))))
 (let (($x1757 (or $x667 (= (+ (- tbl4_kid_5_x) tbl4_kid_2_x) 0.0))))
 (let (($x1754 (or $x667 (= (- tbl4_kid_1_width tbl4_kid_4_width) 0.0))))
 (let (($x1751 (or $x667 (= (- tbl4_kid_1_x tbl4_kid_4_x) 0.0))))
 (let (($x844 (= (- tbl4_kid_0_width tbl4_kid_3_width) 0.0)))
 (let (($x1748 (or $x667 $x844)))
 (let (($x1747 (or $x667 (= (- tbl4_kid_0_x tbl4_kid_3_x) 0.0))))
 (let (($x1744 (or $x667 (= (+ (- tbl4_kid_5_hight) tbl4_kid_3_hight) 0.0))))
 (let (($x1741 (or $x667 (= (+ (- tbl4_kid_5_y) tbl4_kid_3_y) 0.0))))
 (let (($x1738 (or $x667 (= (- tbl4_kid_3_hight tbl4_kid_4_hight) 0.0))))
 (let (($x1735 (or $x667 (= (- tbl4_kid_3_y tbl4_kid_4_y) 0.0))))
 (let (($x755 (= (- tbl4_kid_0_hight tbl4_kid_2_hight) 0.0)))
 (let (($x1732 (or $x667 $x755)))
 (let (($x752 (= (+ (- tbl4_kid_2_y) tbl4_kid_0_y) 0.0)))
 (let (($x1731 (or $x667 $x752)))
 (let (($x748 (= (- tbl4_kid_0_hight tbl4_kid_1_hight) 0.0)))
 (let (($x1730 (or $x667 $x748)))
 (let (($x745 (= (- tbl4_kid_0_y tbl4_kid_1_y) 0.0)))
 (let (($x1729 (or $x667 $x745)))
 (let (($x1727 (= (- (+ (- tbl4_kid_5_y tbl3_hight) tbl4_kid_5_hight) tbl3_y) (- 10.0))))
 (let (($x1728 (or $x667 $x1727)))
 (let (($x1722 (= (+ (- (+ (- tbl3_x) tbl4_kid_5_x) tbl3_width) tbl4_kid_5_width) (- 10.0))))
 (let (($x1723 (or $x667 $x1722)))
 (let (($x1717 (or $x667 (= (- tbl4_kid_0_y tbl3_y) 10.0))))
 (let (($x1714 (or $x667 (= (- tbl4_kid_0_x tbl3_x) 10.0))))
 (let (($x1711 (or $x1617 (= tbl4_kid_7_kid_2_hight 30.0))))
 (let (($x1709 (or $x1617 (= tbl4_kid_7_kid_0_hight 30.0))))
 (let ((?x1701 (- (- tbl4_kid_7_kid_2_y tbl4_kid_7_kid_1_y) tbl4_kid_7_kid_1_hight)))
 (let (($x1707 (or $x1617 (= ?x1701 10.0))))
 (let ((?x1697 (- (- tbl4_kid_7_kid_1_y tbl4_kid_7_kid_0_y) tbl4_kid_7_kid_0_hight)))
 (let (($x1705 (or $x1617 (= ?x1697 10.0))))
 (let (($x1703 (or $x1617 (>= ?x1701 0.0))))
 (let (($x1699 (or $x1617 (>= ?x1697 0.0))))
 (let ((?x1693 (+ (- (- tbl4_kid_7_hight tbl4_kid_7_kid_2_y) tbl4_kid_7_kid_2_hight) tbl4_kid_7_y)))
 (let (($x1695 (or $x1617 (>= ?x1693 20.0))))
 (let (($x1690 (or $x1617 (>= (- tbl4_kid_7_kid_2_y tbl4_kid_7_y) 20.0))))
 (let ((?x1685 (+ (- (- tbl4_kid_7_width tbl4_kid_7_kid_2_x) tbl4_kid_7_kid_2_width) tbl4_kid_7_x)))
 (let (($x1687 (or $x1617 (>= ?x1685 20.0))))
 (let (($x1682 (or $x1617 (>= (- tbl4_kid_7_kid_2_x tbl4_kid_7_x) 20.0))))
 (let ((?x1678 (+ (- (- tbl4_kid_7_hight tbl4_kid_7_kid_1_y) tbl4_kid_7_kid_1_hight) tbl4_kid_7_y)))
 (let (($x1680 (or $x1617 (>= ?x1678 20.0))))
 (let (($x1675 (or $x1617 (>= (- tbl4_kid_7_kid_1_y tbl4_kid_7_y) 20.0))))
 (let ((?x1670 (+ (- (- tbl4_kid_7_width tbl4_kid_7_kid_1_x) tbl4_kid_7_kid_1_width) tbl4_kid_7_x)))
 (let (($x1672 (or $x1617 (>= ?x1670 20.0))))
 (let (($x1667 (or $x1617 (>= (- tbl4_kid_7_kid_1_x tbl4_kid_7_x) 20.0))))
 (let ((?x1663 (- (+ (- tbl4_kid_7_hight tbl4_kid_7_kid_0_y) tbl4_kid_7_y) tbl4_kid_7_kid_0_hight)))
 (let (($x1665 (or $x1617 (>= ?x1663 20.0))))
 (let (($x1660 (or $x1617 (>= (- tbl4_kid_7_kid_0_y tbl4_kid_7_y) 20.0))))
 (let ((?x1655 (- (+ (- tbl4_kid_7_kid_0_width) tbl4_kid_7_width) tbl4_kid_7_kid_0_x)))
 (let (($x1658 (or $x1617 (>= (+ ?x1655 tbl4_kid_7_x) 20.0))))
 (let (($x1652 (or $x1617 (>= (- tbl4_kid_7_kid_0_x tbl4_kid_7_x) 20.0))))
 (let (($x1650 (= tbl4_kid_7_hight 350.0)))
 (let ((?x1646 (+ (+ (- tbl4_kid_7_hight) tbl4_kid_7_kid_2_y) tbl4_kid_7_kid_2_hight)))
 (let (($x1649 (or $x1617 (= (- ?x1646 tbl4_kid_7_y) (- 20.0)))))
 (let (($x1644 (or $x1617 (= (- tbl4_kid_7_kid_0_y tbl4_kid_7_y) 20.0))))
 (let ((?x1638 (+ (+ (- tbl4_kid_7_width) tbl4_kid_7_kid_2_x) tbl4_kid_7_kid_2_width)))
 (let (($x1641 (or $x1617 (= (- ?x1638 tbl4_kid_7_x) (- 20.0)))))
 (let ((?x1633 (+ (+ (- tbl4_kid_7_width) tbl4_kid_7_kid_1_x) tbl4_kid_7_kid_1_width)))
 (let (($x1636 (or $x1617 (= (- ?x1633 tbl4_kid_7_x) (- 20.0)))))
 (let ((?x1629 (- (+ (- tbl4_kid_7_kid_0_width tbl4_kid_7_width) tbl4_kid_7_kid_0_x) tbl4_kid_7_x)))
 (let (($x1631 (or $x1617 (= ?x1629 (- 20.0)))))
 (let (($x1626 (or $x1617 (= (- tbl4_kid_7_kid_2_x tbl4_kid_7_x) 20.0))))
 (let (($x1623 (or $x1617 (= (- tbl4_kid_7_kid_1_x tbl4_kid_7_x) 20.0))))
 (let (($x1620 (or $x1617 (= (- tbl4_kid_7_kid_0_x tbl4_kid_7_x) 20.0))))
 (let (($x1616 (>= tbl4_kid_7_kid_2_hight 0.0)))
 (let (($x1615 (>= tbl4_kid_7_kid_2_width 0.0)))
 (let (($x1614 (>= tbl4_kid_7_kid_2_y 0.0)))
 (let (($x1613 (>= tbl4_kid_7_kid_2_x 0.0)))
 (let (($x1612 (>= tbl4_kid_7_kid_1_hight 0.0)))
 (let (($x1611 (>= tbl4_kid_7_kid_1_width 0.0)))
 (let (($x1610 (>= tbl4_kid_7_kid_1_y 0.0)))
 (let (($x1609 (>= tbl4_kid_7_kid_1_x 0.0)))
 (let (($x1608 (>= tbl4_kid_7_kid_0_hight 0.0)))
 (let (($x1607 (>= tbl4_kid_7_kid_0_width 0.0)))
 (let (($x1606 (>= tbl4_kid_7_kid_0_y 0.0)))
 (let (($x1605 (>= tbl4_kid_7_kid_0_x 0.0)))
 (let (($x1604 (or $x1509 (= tbl4_kid_6_kid_2_hight 30.0))))
 (let (($x1602 (or $x1509 (= tbl4_kid_6_kid_0_hight 30.0))))
 (let ((?x1594 (- (- tbl4_kid_6_kid_2_y tbl4_kid_6_kid_1_y) tbl4_kid_6_kid_1_hight)))
 (let (($x1600 (or $x1509 (= ?x1594 10.0))))
 (let ((?x1590 (- (+ (- tbl4_kid_6_kid_0_hight) tbl4_kid_6_kid_1_y) tbl4_kid_6_kid_0_y)))
 (let (($x1598 (or $x1509 (= ?x1590 10.0))))
 (let (($x1596 (or $x1509 (>= ?x1594 0.0))))
 (let (($x1592 (or $x1509 (>= ?x1590 0.0))))
 (let ((?x1585 (+ (- (- tbl4_kid_6_hight tbl4_kid_6_kid_2_y) tbl4_kid_6_kid_2_hight) tbl4_kid_6_y)))
 (let (($x1587 (or $x1509 (>= ?x1585 20.0))))
 (let (($x1582 (or $x1509 (>= (- tbl4_kid_6_kid_2_y tbl4_kid_6_y) 20.0))))
 (let ((?x1577 (- (+ (+ (- tbl4_kid_6_kid_2_width) tbl4_kid_6_x) tbl4_kid_6_width) tbl4_kid_6_kid_2_x)))
 (let (($x1579 (or $x1509 (>= ?x1577 20.0))))
 (let (($x1573 (or $x1509 (>= (+ (- tbl4_kid_6_x) tbl4_kid_6_kid_2_x) 20.0))))
 (let ((?x1569 (- (+ (- tbl4_kid_6_hight tbl4_kid_6_kid_1_y) tbl4_kid_6_y) tbl4_kid_6_kid_1_hight)))
 (let (($x1571 (or $x1509 (>= ?x1569 20.0))))
 (let (($x1566 (or $x1509 (>= (- tbl4_kid_6_kid_1_y tbl4_kid_6_y) 20.0))))
 (let ((?x1561 (+ (- (+ (- tbl4_kid_6_kid_1_x) tbl4_kid_6_x) tbl4_kid_6_kid_1_width) tbl4_kid_6_width)))
 (let (($x1563 (or $x1509 (>= ?x1561 20.0))))
 (let (($x1557 (or $x1509 (>= (- tbl4_kid_6_kid_1_x tbl4_kid_6_x) 20.0))))
 (let ((?x1553 (- (+ (- tbl4_kid_6_hight tbl4_kid_6_kid_0_hight) tbl4_kid_6_y) tbl4_kid_6_kid_0_y)))
 (let (($x1555 (or $x1509 (>= ?x1553 20.0))))
 (let (($x1550 (or $x1509 (>= (+ (- tbl4_kid_6_y) tbl4_kid_6_kid_0_y) 20.0))))
 (let ((?x1546 (- (+ (- tbl4_kid_6_x tbl4_kid_6_kid_0_x) tbl4_kid_6_width) tbl4_kid_6_kid_0_width)))
 (let (($x1548 (or $x1509 (>= ?x1546 20.0))))
 (let (($x1543 (or $x1509 (>= (+ (- tbl4_kid_6_x) tbl4_kid_6_kid_0_x) 20.0))))
 (let (($x1541 (= tbl4_kid_6_hight 350.0)))
 (let ((?x1537 (+ (+ (- tbl4_kid_6_hight) tbl4_kid_6_kid_2_y) tbl4_kid_6_kid_2_hight)))
 (let (($x1540 (or $x1509 (= (- ?x1537 tbl4_kid_6_y) (- 20.0)))))
 (let (($x1535 (or $x1509 (= (+ (- tbl4_kid_6_y) tbl4_kid_6_kid_0_y) 20.0))))
 (let ((?x1529 (+ (- (- tbl4_kid_6_kid_2_width tbl4_kid_6_x) tbl4_kid_6_width) tbl4_kid_6_kid_2_x)))
 (let (($x1531 (or $x1509 (= ?x1529 (- 20.0)))))
 (let ((?x1524 (- (+ (- tbl4_kid_6_kid_1_x tbl4_kid_6_x) tbl4_kid_6_kid_1_width) tbl4_kid_6_width)))
 (let (($x1526 (or $x1509 (= ?x1524 (- 20.0)))))
 (let ((?x1520 (+ (- (+ (- tbl4_kid_6_x) tbl4_kid_6_kid_0_x) tbl4_kid_6_width) tbl4_kid_6_kid_0_width)))
 (let (($x1522 (or $x1509 (= ?x1520 (- 20.0)))))
 (let (($x1518 (or $x1509 (= (+ (- tbl4_kid_6_x) tbl4_kid_6_kid_2_x) 20.0))))
 (let (($x1515 (or $x1509 (= (- tbl4_kid_6_kid_1_x tbl4_kid_6_x) 20.0))))
 (let (($x1512 (or $x1509 (= (+ (- tbl4_kid_6_x) tbl4_kid_6_kid_0_x) 20.0))))
 (let (($x1508 (>= tbl4_kid_6_kid_2_hight 0.0)))
 (let (($x1507 (>= tbl4_kid_6_kid_2_width 0.0)))
 (let (($x1506 (>= tbl4_kid_6_kid_2_y 0.0)))
 (let (($x1505 (>= tbl4_kid_6_kid_2_x 0.0)))
 (let (($x1504 (>= tbl4_kid_6_kid_1_hight 0.0)))
 (let (($x1503 (>= tbl4_kid_6_kid_1_width 0.0)))
 (let (($x1502 (>= tbl4_kid_6_kid_1_y 0.0)))
 (let (($x1501 (>= tbl4_kid_6_kid_1_x 0.0)))
 (let (($x1500 (>= tbl4_kid_6_kid_0_hight 0.0)))
 (let (($x1499 (>= tbl4_kid_6_kid_0_width 0.0)))
 (let (($x1498 (>= tbl4_kid_6_kid_0_y 0.0)))
 (let (($x1497 (>= tbl4_kid_6_kid_0_x 0.0)))
 (let (($x1496 (or $x1403 (= tbl4_kid_5_kid_2_hight 30.0))))
 (let (($x1494 (or $x1403 (= tbl4_kid_5_kid_0_hight 30.0))))
 (let ((?x1486 (+ (- (- tbl4_kid_5_kid_1_y) tbl4_kid_5_kid_1_hight) tbl4_kid_5_kid_2_y)))
 (let (($x1492 (or $x1403 (= ?x1486 10.0))))
 (let ((?x1481 (- (- tbl4_kid_5_kid_1_y tbl4_kid_5_kid_0_y) tbl4_kid_5_kid_0_hight)))
 (let (($x1490 (or $x1403 (= ?x1481 10.0))))
 (let (($x1488 (or $x1403 (>= ?x1486 0.0))))
 (let (($x1483 (or $x1403 (>= ?x1481 0.0))))
 (let ((?x1477 (- (- (+ tbl4_kid_5_y tbl4_kid_5_hight) tbl4_kid_5_kid_2_hight) tbl4_kid_5_kid_2_y)))
 (let (($x1479 (or $x1403 (>= ?x1477 20.0))))
 (let (($x1475 (or $x1403 (>= (+ (- tbl4_kid_5_y) tbl4_kid_5_kid_2_y) 20.0))))
 (let ((?x1470 (- (+ (+ (- tbl4_kid_5_kid_2_x) tbl4_kid_5_x) tbl4_kid_5_width) tbl4_kid_5_kid_2_width)))
 (let (($x1472 (or $x1403 (>= ?x1470 20.0))))
 (let (($x1466 (or $x1403 (>= (- tbl4_kid_5_kid_2_x tbl4_kid_5_x) 20.0))))
 (let ((?x1462 (- (+ (- tbl4_kid_5_y tbl4_kid_5_kid_1_y) tbl4_kid_5_hight) tbl4_kid_5_kid_1_hight)))
 (let (($x1464 (or $x1403 (>= ?x1462 20.0))))
 (let (($x1459 (or $x1403 (>= (+ (- tbl4_kid_5_y) tbl4_kid_5_kid_1_y) 20.0))))
 (let ((?x1454 (- (+ (- tbl4_kid_5_x tbl4_kid_5_kid_1_x) tbl4_kid_5_width) tbl4_kid_5_kid_1_width)))
 (let (($x1456 (or $x1403 (>= ?x1454 20.0))))
 (let (($x1451 (or $x1403 (>= (+ (- tbl4_kid_5_x) tbl4_kid_5_kid_1_x) 20.0))))
 (let ((?x1447 (- (- (+ tbl4_kid_5_y tbl4_kid_5_hight) tbl4_kid_5_kid_0_y) tbl4_kid_5_kid_0_hight)))
 (let (($x1449 (or $x1403 (>= ?x1447 20.0))))
 (let (($x1444 (or $x1403 (>= (+ (- tbl4_kid_5_y) tbl4_kid_5_kid_0_y) 20.0))))
 (let ((?x1440 (- (- (+ tbl4_kid_5_x tbl4_kid_5_width) tbl4_kid_5_kid_0_x) tbl4_kid_5_kid_0_width)))
 (let (($x1442 (or $x1403 (>= ?x1440 20.0))))
 (let (($x1437 (or $x1403 (>= (+ (- tbl4_kid_5_x) tbl4_kid_5_kid_0_x) 20.0))))
 (let (($x1435 (= tbl4_kid_5_hight 350.0)))
 (let ((?x1432 (+ (+ (- (- tbl4_kid_5_y) tbl4_kid_5_hight) tbl4_kid_5_kid_2_hight) tbl4_kid_5_kid_2_y)))
 (let (($x1434 (or $x1403 (= ?x1432 (- 20.0)))))
 (let (($x1429 (or $x1403 (= (+ (- tbl4_kid_5_y) tbl4_kid_5_kid_0_y) 20.0))))
 (let ((?x1424 (+ (- (- tbl4_kid_5_kid_2_x tbl4_kid_5_x) tbl4_kid_5_width) tbl4_kid_5_kid_2_width)))
 (let (($x1426 (or $x1403 (= ?x1424 (- 20.0)))))
 (let ((?x1420 (+ (- (+ (- tbl4_kid_5_x) tbl4_kid_5_kid_1_x) tbl4_kid_5_width) tbl4_kid_5_kid_1_width)))
 (let (($x1422 (or $x1403 (= ?x1420 (- 20.0)))))
 (let ((?x1416 (+ (+ (- (- tbl4_kid_5_x) tbl4_kid_5_width) tbl4_kid_5_kid_0_x) tbl4_kid_5_kid_0_width)))
 (let (($x1418 (or $x1403 (= ?x1416 (- 20.0)))))
 (let (($x1413 (or $x1403 (= (- tbl4_kid_5_kid_2_x tbl4_kid_5_x) 20.0))))
 (let (($x1410 (or $x1403 (= (+ (- tbl4_kid_5_x) tbl4_kid_5_kid_1_x) 20.0))))
 (let (($x1407 (or $x1403 (= (+ (- tbl4_kid_5_x) tbl4_kid_5_kid_0_x) 20.0))))
 (let (($x1402 (>= tbl4_kid_5_kid_2_hight 0.0)))
 (let (($x1401 (>= tbl4_kid_5_kid_2_width 0.0)))
 (let (($x1400 (>= tbl4_kid_5_kid_2_y 0.0)))
 (let (($x1399 (>= tbl4_kid_5_kid_2_x 0.0)))
 (let (($x1398 (>= tbl4_kid_5_kid_1_hight 0.0)))
 (let (($x1397 (>= tbl4_kid_5_kid_1_width 0.0)))
 (let (($x1396 (>= tbl4_kid_5_kid_1_y 0.0)))
 (let (($x1395 (>= tbl4_kid_5_kid_1_x 0.0)))
 (let (($x1394 (>= tbl4_kid_5_kid_0_hight 0.0)))
 (let (($x1393 (>= tbl4_kid_5_kid_0_width 0.0)))
 (let (($x1392 (>= tbl4_kid_5_kid_0_y 0.0)))
 (let (($x1391 (>= tbl4_kid_5_kid_0_x 0.0)))
 (let (($x1390 (or $x1293 (= tbl4_kid_4_kid_2_hight 30.0))))
 (let (($x1388 (or $x1293 (= tbl4_kid_4_kid_0_hight 30.0))))
 (let ((?x1380 (- (+ (- tbl4_kid_4_kid_1_y) tbl4_kid_4_kid_2_y) tbl4_kid_4_kid_1_hight)))
 (let (($x1386 (or $x1293 (= ?x1380 10.0))))
 (let ((?x1375 (- (- tbl4_kid_4_kid_1_y tbl4_kid_4_kid_0_y) tbl4_kid_4_kid_0_hight)))
 (let (($x1384 (or $x1293 (= ?x1375 10.0))))
 (let (($x1382 (or $x1293 (>= ?x1380 0.0))))
 (let (($x1377 (or $x1293 (>= ?x1375 0.0))))
 (let ((?x1371 (- (- (+ tbl4_kid_4_y tbl4_kid_4_hight) tbl4_kid_4_kid_2_y) tbl4_kid_4_kid_2_hight)))
 (let (($x1373 (or $x1293 (>= ?x1371 20.0))))
 (let (($x1369 (or $x1293 (>= (+ (- tbl4_kid_4_y) tbl4_kid_4_kid_2_y) 20.0))))
 (let ((?x1364 (- (+ (+ (- tbl4_kid_4_kid_2_width) tbl4_kid_4_x) tbl4_kid_4_width) tbl4_kid_4_kid_2_x)))
 (let (($x1366 (or $x1293 (>= ?x1364 20.0))))
 (let (($x1360 (or $x1293 (>= (+ (- tbl4_kid_4_x) tbl4_kid_4_kid_2_x) 20.0))))
 (let ((?x1356 (- (- (+ tbl4_kid_4_y tbl4_kid_4_hight) tbl4_kid_4_kid_1_y) tbl4_kid_4_kid_1_hight)))
 (let (($x1358 (or $x1293 (>= ?x1356 20.0))))
 (let (($x1354 (or $x1293 (>= (+ (- tbl4_kid_4_y) tbl4_kid_4_kid_1_y) 20.0))))
 (let ((?x1349 (- (+ (+ (- tbl4_kid_4_kid_1_width) tbl4_kid_4_x) tbl4_kid_4_width) tbl4_kid_4_kid_1_x)))
 (let (($x1351 (or $x1293 (>= ?x1349 20.0))))
 (let (($x1345 (or $x1293 (>= (+ (- tbl4_kid_4_x) tbl4_kid_4_kid_1_x) 20.0))))
 (let ((?x1341 (- (- (+ tbl4_kid_4_y tbl4_kid_4_hight) tbl4_kid_4_kid_0_y) tbl4_kid_4_kid_0_hight)))
 (let (($x1343 (or $x1293 (>= ?x1341 20.0))))
 (let (($x1338 (or $x1293 (>= (+ (- tbl4_kid_4_y) tbl4_kid_4_kid_0_y) 20.0))))
 (let ((?x1334 (+ (+ (- (- tbl4_kid_4_kid_0_x) tbl4_kid_4_kid_0_width) tbl4_kid_4_x) tbl4_kid_4_width)))
 (let (($x1336 (or $x1293 (>= ?x1334 20.0))))
 (let (($x1330 (or $x1293 (>= (- tbl4_kid_4_kid_0_x tbl4_kid_4_x) 20.0))))
 (let (($x1328 (= tbl4_kid_4_hight 350.0)))
 (let ((?x1325 (+ (+ (- (- tbl4_kid_4_y) tbl4_kid_4_hight) tbl4_kid_4_kid_2_y) tbl4_kid_4_kid_2_hight)))
 (let (($x1327 (or $x1293 (= ?x1325 (- 20.0)))))
 (let (($x1322 (or $x1293 (= (+ (- tbl4_kid_4_y) tbl4_kid_4_kid_0_y) 20.0))))
 (let ((?x1316 (+ (- (- tbl4_kid_4_kid_2_width tbl4_kid_4_x) tbl4_kid_4_width) tbl4_kid_4_kid_2_x)))
 (let (($x1318 (or $x1293 (= ?x1316 (- 20.0)))))
 (let ((?x1311 (+ (- (- tbl4_kid_4_kid_1_width tbl4_kid_4_x) tbl4_kid_4_width) tbl4_kid_4_kid_1_x)))
 (let (($x1313 (or $x1293 (= ?x1311 (- 20.0)))))
 (let ((?x1306 (- (- (+ tbl4_kid_4_kid_0_x tbl4_kid_4_kid_0_width) tbl4_kid_4_x) tbl4_kid_4_width)))
 (let (($x1308 (or $x1293 (= ?x1306 (- 20.0)))))
 (let (($x1303 (or $x1293 (= (+ (- tbl4_kid_4_x) tbl4_kid_4_kid_2_x) 20.0))))
 (let (($x1300 (or $x1293 (= (+ (- tbl4_kid_4_x) tbl4_kid_4_kid_1_x) 20.0))))
 (let (($x1296 (or $x1293 (= (- tbl4_kid_4_kid_0_x tbl4_kid_4_x) 20.0))))
 (let (($x1292 (>= tbl4_kid_4_kid_2_hight 0.0)))
 (let (($x1291 (>= tbl4_kid_4_kid_2_width 0.0)))
 (let (($x1290 (>= tbl4_kid_4_kid_2_y 0.0)))
 (let (($x1289 (>= tbl4_kid_4_kid_2_x 0.0)))
 (let (($x1288 (>= tbl4_kid_4_kid_1_hight 0.0)))
 (let (($x1287 (>= tbl4_kid_4_kid_1_width 0.0)))
 (let (($x1286 (>= tbl4_kid_4_kid_1_y 0.0)))
 (let (($x1285 (>= tbl4_kid_4_kid_1_x 0.0)))
 (let (($x1284 (>= tbl4_kid_4_kid_0_hight 0.0)))
 (let (($x1283 (>= tbl4_kid_4_kid_0_width 0.0)))
 (let (($x1282 (>= tbl4_kid_4_kid_0_y 0.0)))
 (let (($x1281 (>= tbl4_kid_4_kid_0_x 0.0)))
 (let (($x1280 (or $x1183 (= tbl4_kid_3_kid_2_hight 30.0))))
 (let (($x1278 (or $x1183 (= tbl4_kid_3_kid_0_hight 30.0))))
 (let ((?x1270 (+ (- (- tbl4_kid_3_kid_1_y) tbl4_kid_3_kid_1_hight) tbl4_kid_3_kid_2_y)))
 (let (($x1276 (or $x1183 (= ?x1270 10.0))))
 (let ((?x1266 (- (+ (- tbl4_kid_3_kid_0_y) tbl4_kid_3_kid_1_y) tbl4_kid_3_kid_0_hight)))
 (let (($x1274 (or $x1183 (= ?x1266 10.0))))
 (let (($x1272 (or $x1183 (>= ?x1270 0.0))))
 (let (($x1268 (or $x1183 (>= ?x1266 0.0))))
 (let ((?x1262 (- (+ (+ (- tbl4_kid_3_kid_2_hight) tbl4_kid_3_y) tbl4_kid_3_hight) tbl4_kid_3_kid_2_y)))
 (let (($x1264 (or $x1183 (>= ?x1262 20.0))))
 (let (($x1258 (or $x1183 (>= (+ (- tbl4_kid_3_y) tbl4_kid_3_kid_2_y) 20.0))))
 (let ((?x1253 (+ (+ (- (- tbl4_kid_3_kid_2_x) tbl4_kid_3_kid_2_width) tbl4_kid_3_x) tbl4_kid_3_width)))
 (let (($x1255 (or $x1183 (>= ?x1253 20.0))))
 (let (($x1249 (or $x1183 (>= (- tbl4_kid_3_kid_2_x tbl4_kid_3_x) 20.0))))
 (let ((?x1245 (+ (- (+ (- tbl4_kid_3_kid_1_y) tbl4_kid_3_y) tbl4_kid_3_kid_1_hight) tbl4_kid_3_hight)))
 (let (($x1247 (or $x1183 (>= ?x1245 20.0))))
 (let (($x1241 (or $x1183 (>= (- tbl4_kid_3_kid_1_y tbl4_kid_3_y) 20.0))))
 (let ((?x1236 (+ (- (+ (- tbl4_kid_3_kid_1_x) tbl4_kid_3_x) tbl4_kid_3_kid_1_width) tbl4_kid_3_width)))
 (let (($x1238 (or $x1183 (>= ?x1236 20.0))))
 (let (($x1232 (or $x1183 (>= (- tbl4_kid_3_kid_1_x tbl4_kid_3_x) 20.0))))
 (let ((?x1228 (+ (- (+ (- tbl4_kid_3_kid_0_y) tbl4_kid_3_y) tbl4_kid_3_kid_0_hight) tbl4_kid_3_hight)))
 (let (($x1230 (or $x1183 (>= ?x1228 20.0))))
 (let (($x1224 (or $x1183 (>= (- tbl4_kid_3_kid_0_y tbl4_kid_3_y) 20.0))))
 (let ((?x1220 (+ (- (+ (- tbl4_kid_3_kid_0_x) tbl4_kid_3_x) tbl4_kid_3_kid_0_width) tbl4_kid_3_width)))
 (let (($x1222 (or $x1183 (>= ?x1220 20.0))))
 (let (($x1216 (or $x1183 (>= (- tbl4_kid_3_kid_0_x tbl4_kid_3_x) 20.0))))
 (let (($x1214 (= tbl4_kid_3_hight 350.0)))
 (let ((?x1211 (+ (- (- tbl4_kid_3_kid_2_hight tbl4_kid_3_y) tbl4_kid_3_hight) tbl4_kid_3_kid_2_y)))
 (let (($x1213 (or $x1183 (= ?x1211 (- 20.0)))))
 (let (($x1208 (or $x1183 (= (- tbl4_kid_3_kid_0_y tbl4_kid_3_y) 20.0))))
 (let ((?x1203 (- (- (+ tbl4_kid_3_kid_2_x tbl4_kid_3_kid_2_width) tbl4_kid_3_x) tbl4_kid_3_width)))
 (let (($x1205 (or $x1183 (= ?x1203 (- 20.0)))))
 (let ((?x1198 (- (+ (- tbl4_kid_3_kid_1_x tbl4_kid_3_x) tbl4_kid_3_kid_1_width) tbl4_kid_3_width)))
 (let (($x1200 (or $x1183 (= ?x1198 (- 20.0)))))
 (let ((?x1194 (- (+ (- tbl4_kid_3_kid_0_x tbl4_kid_3_x) tbl4_kid_3_kid_0_width) tbl4_kid_3_width)))
 (let (($x1196 (or $x1183 (= ?x1194 (- 20.0)))))
 (let (($x1192 (or $x1183 (= (- tbl4_kid_3_kid_2_x tbl4_kid_3_x) 20.0))))
 (let (($x1189 (or $x1183 (= (- tbl4_kid_3_kid_1_x tbl4_kid_3_x) 20.0))))
 (let (($x1186 (or $x1183 (= (- tbl4_kid_3_kid_0_x tbl4_kid_3_x) 20.0))))
 (let (($x1182 (>= tbl4_kid_3_kid_2_hight 0.0)))
 (let (($x1181 (>= tbl4_kid_3_kid_2_width 0.0)))
 (let (($x1180 (>= tbl4_kid_3_kid_2_y 0.0)))
 (let (($x1179 (>= tbl4_kid_3_kid_2_x 0.0)))
 (let (($x1178 (>= tbl4_kid_3_kid_1_hight 0.0)))
 (let (($x1177 (>= tbl4_kid_3_kid_1_width 0.0)))
 (let (($x1176 (>= tbl4_kid_3_kid_1_y 0.0)))
 (let (($x1175 (>= tbl4_kid_3_kid_1_x 0.0)))
 (let (($x1174 (>= tbl4_kid_3_kid_0_hight 0.0)))
 (let (($x1173 (>= tbl4_kid_3_kid_0_width 0.0)))
 (let (($x1172 (>= tbl4_kid_3_kid_0_y 0.0)))
 (let (($x1171 (>= tbl4_kid_3_kid_0_x 0.0)))
 (let (($x1170 (or $x1074 (= tbl4_kid_2_kid_2_hight 30.0))))
 (let (($x1168 (or $x1074 (= tbl4_kid_2_kid_0_hight 30.0))))
 (let ((?x1160 (- (- tbl4_kid_2_kid_2_y tbl4_kid_2_kid_1_y) tbl4_kid_2_kid_1_hight)))
 (let (($x1166 (or $x1074 (= ?x1160 10.0))))
 (let ((?x1156 (+ (- (- tbl4_kid_2_kid_0_hight) tbl4_kid_2_kid_0_y) tbl4_kid_2_kid_1_y)))
 (let (($x1164 (or $x1074 (= ?x1156 10.0))))
 (let (($x1162 (or $x1074 (>= ?x1160 0.0))))
 (let (($x1158 (or $x1074 (>= ?x1156 0.0))))
 (let ((?x1152 (+ (- (+ (- tbl4_kid_2_kid_2_y) tbl4_kid_2_y) tbl4_kid_2_kid_2_hight) tbl4_kid_2_hight)))
 (let (($x1154 (or $x1074 (>= ?x1152 20.0))))
 (let (($x1148 (or $x1074 (>= (- tbl4_kid_2_kid_2_y tbl4_kid_2_y) 20.0))))
 (let ((?x1143 (- (+ (- tbl4_kid_2_kid_2_width) tbl4_kid_2_width) tbl4_kid_2_kid_2_x)))
 (let (($x1146 (or $x1074 (>= (+ ?x1143 tbl4_kid_2_x) 20.0))))
 (let (($x1140 (or $x1074 (>= (- tbl4_kid_2_kid_2_x tbl4_kid_2_x) 20.0))))
 (let ((?x1136 (- (+ (- tbl4_kid_2_y tbl4_kid_2_kid_1_y) tbl4_kid_2_hight) tbl4_kid_2_kid_1_hight)))
 (let (($x1138 (or $x1074 (>= ?x1136 20.0))))
 (let (($x1133 (or $x1074 (>= (+ (- tbl4_kid_2_y) tbl4_kid_2_kid_1_y) 20.0))))
 (let ((?x1128 (- (+ (- tbl4_kid_2_width tbl4_kid_2_kid_1_width) tbl4_kid_2_x) tbl4_kid_2_kid_1_x)))
 (let (($x1130 (or $x1074 (>= ?x1128 20.0))))
 (let (($x1125 (or $x1074 (>= (+ (- tbl4_kid_2_x) tbl4_kid_2_kid_1_x) 20.0))))
 (let ((?x1121 (+ (- (+ (- tbl4_kid_2_kid_0_hight) tbl4_kid_2_y) tbl4_kid_2_kid_0_y) tbl4_kid_2_hight)))
 (let (($x1123 (or $x1074 (>= ?x1121 20.0))))
 (let (($x1117 (or $x1074 (>= (+ (- tbl4_kid_2_y) tbl4_kid_2_kid_0_y) 20.0))))
 (let ((?x1113 (- (+ (- tbl4_kid_2_width tbl4_kid_2_kid_0_width) tbl4_kid_2_x) tbl4_kid_2_kid_0_x)))
 (let (($x1115 (or $x1074 (>= ?x1113 20.0))))
 (let (($x1110 (or $x1074 (>= (+ (- tbl4_kid_2_x) tbl4_kid_2_kid_0_x) 20.0))))
 (let (($x1108 (= tbl4_kid_2_hight 350.0)))
 (let ((?x1105 (- (+ (- tbl4_kid_2_kid_2_y tbl4_kid_2_y) tbl4_kid_2_kid_2_hight) tbl4_kid_2_hight)))
 (let (($x1107 (or $x1074 (= ?x1105 (- 20.0)))))
 (let (($x1102 (or $x1074 (= (+ (- tbl4_kid_2_y) tbl4_kid_2_kid_0_y) 20.0))))
 (let ((?x1097 (- (+ (- tbl4_kid_2_kid_2_width tbl4_kid_2_width) tbl4_kid_2_kid_2_x) tbl4_kid_2_x)))
 (let (($x1099 (or $x1074 (= ?x1097 (- 20.0)))))
 (let ((?x1092 (+ (- (+ (- tbl4_kid_2_width) tbl4_kid_2_kid_1_width) tbl4_kid_2_x) tbl4_kid_2_kid_1_x)))
 (let (($x1094 (or $x1074 (= ?x1092 (- 20.0)))))
 (let ((?x1087 (+ (- (+ (- tbl4_kid_2_width) tbl4_kid_2_kid_0_width) tbl4_kid_2_x) tbl4_kid_2_kid_0_x)))
 (let (($x1089 (or $x1074 (= ?x1087 (- 20.0)))))
 (let (($x1084 (or $x1074 (= (- tbl4_kid_2_kid_2_x tbl4_kid_2_x) 20.0))))
 (let (($x1081 (or $x1074 (= (+ (- tbl4_kid_2_x) tbl4_kid_2_kid_1_x) 20.0))))
 (let (($x1078 (or $x1074 (= (+ (- tbl4_kid_2_x) tbl4_kid_2_kid_0_x) 20.0))))
 (let (($x1073 (>= tbl4_kid_2_kid_2_hight 0.0)))
 (let (($x1072 (>= tbl4_kid_2_kid_2_width 0.0)))
 (let (($x1071 (>= tbl4_kid_2_kid_2_y 0.0)))
 (let (($x1070 (>= tbl4_kid_2_kid_2_x 0.0)))
 (let (($x1069 (>= tbl4_kid_2_kid_1_hight 0.0)))
 (let (($x1068 (>= tbl4_kid_2_kid_1_width 0.0)))
 (let (($x1067 (>= tbl4_kid_2_kid_1_y 0.0)))
 (let (($x1066 (>= tbl4_kid_2_kid_1_x 0.0)))
 (let (($x1065 (>= tbl4_kid_2_kid_0_hight 0.0)))
 (let (($x1064 (>= tbl4_kid_2_kid_0_width 0.0)))
 (let (($x1063 (>= tbl4_kid_2_kid_0_y 0.0)))
 (let (($x1062 (>= tbl4_kid_2_kid_0_x 0.0)))
 (let (($x1061 (or $x967 (= tbl4_kid_1_kid_2_hight 30.0))))
 (let (($x1059 (or $x967 (= tbl4_kid_1_kid_0_hight 30.0))))
 (let ((?x1025 (- (- tbl4_kid_1_kid_1_y) tbl4_kid_1_kid_1_hight)))
 (let ((?x1051 (+ ?x1025 tbl4_kid_1_kid_2_y)))
 (let (($x1057 (or $x967 (= ?x1051 10.0))))
 (let ((?x1048 (- (- tbl4_kid_1_kid_1_y tbl4_kid_1_kid_0_y) tbl4_kid_1_kid_0_hight)))
 (let (($x1055 (or $x967 (= ?x1048 10.0))))
 (let (($x1053 (or $x967 (>= ?x1051 0.0))))
 (let (($x1050 (or $x967 (>= ?x1048 0.0))))
 (let ((?x1044 (+ (- (+ (- tbl4_kid_1_kid_2_hight) tbl4_kid_1_y) tbl4_kid_1_kid_2_y) tbl4_kid_1_hight)))
 (let (($x1046 (or $x967 (>= ?x1044 20.0))))
 (let (($x1040 (or $x967 (>= (+ (- tbl4_kid_1_y) tbl4_kid_1_kid_2_y) 20.0))))
 (let ((?x1034 (- (+ (- tbl4_kid_1_x tbl4_kid_1_kid_2_x) tbl4_kid_1_width) tbl4_kid_1_kid_2_width)))
 (let (($x1036 (or $x967 (>= ?x1034 20.0))))
 (let (($x1031 (or $x967 (>= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_2_x) 20.0))))
 (let (($x1029 (or $x967 (>= (+ (+ ?x1025 tbl4_kid_1_y) tbl4_kid_1_hight) 20.0))))
 (let (($x1023 (or $x967 (>= (- tbl4_kid_1_kid_1_y tbl4_kid_1_y) 20.0))))
 (let ((?x1018 (- (- (+ tbl4_kid_1_x tbl4_kid_1_width) tbl4_kid_1_kid_1_x) tbl4_kid_1_kid_1_width)))
 (let (($x1020 (or $x967 (>= ?x1018 20.0))))
 (let (($x1016 (or $x967 (>= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_1_x) 20.0))))
 (let ((?x1012 (+ (+ (- (- tbl4_kid_1_kid_0_y) tbl4_kid_1_kid_0_hight) tbl4_kid_1_y) tbl4_kid_1_hight)))
 (let (($x1014 (or $x967 (>= ?x1012 20.0))))
 (let (($x1008 (or $x967 (>= (- tbl4_kid_1_kid_0_y tbl4_kid_1_y) 20.0))))
 (let ((?x1004 (- (- (+ tbl4_kid_1_x tbl4_kid_1_width) tbl4_kid_1_kid_0_x) tbl4_kid_1_kid_0_width)))
 (let (($x1006 (or $x967 (>= ?x1004 20.0))))
 (let (($x1001 (or $x967 (>= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_0_x) 20.0))))
 (let (($x999 (= tbl4_kid_1_hight 350.0)))
 (let ((?x996 (- (+ (- tbl4_kid_1_kid_2_hight tbl4_kid_1_y) tbl4_kid_1_kid_2_y) tbl4_kid_1_hight)))
 (let (($x998 (or $x967 (= ?x996 (- 20.0)))))
 (let (($x993 (or $x967 (= (- tbl4_kid_1_kid_0_y tbl4_kid_1_y) 20.0))))
 (let ((?x988 (+ (- (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_2_x) tbl4_kid_1_width) tbl4_kid_1_kid_2_width)))
 (let (($x990 (or $x967 (= ?x988 (- 20.0)))))
 (let ((?x984 (+ (+ (- (- tbl4_kid_1_x) tbl4_kid_1_width) tbl4_kid_1_kid_1_x) tbl4_kid_1_kid_1_width)))
 (let (($x986 (or $x967 (= ?x984 (- 20.0)))))
 (let ((?x980 (+ (+ (- (- tbl4_kid_1_x) tbl4_kid_1_width) tbl4_kid_1_kid_0_x) tbl4_kid_1_kid_0_width)))
 (let (($x982 (or $x967 (= ?x980 (- 20.0)))))
 (let (($x977 (or $x967 (= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_2_x) 20.0))))
 (let (($x974 (or $x967 (= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_1_x) 20.0))))
 (let (($x971 (or $x967 (= (+ (- tbl4_kid_1_x) tbl4_kid_1_kid_0_x) 20.0))))
 (let (($x966 (>= tbl4_kid_1_kid_2_hight 0.0)))
 (let (($x965 (>= tbl4_kid_1_kid_2_width 0.0)))
 (let (($x964 (>= tbl4_kid_1_kid_2_y 0.0)))
 (let (($x963 (>= tbl4_kid_1_kid_2_x 0.0)))
 (let (($x962 (>= tbl4_kid_1_kid_1_hight 0.0)))
 (let (($x961 (>= tbl4_kid_1_kid_1_width 0.0)))
 (let (($x960 (>= tbl4_kid_1_kid_1_y 0.0)))
 (let (($x959 (>= tbl4_kid_1_kid_1_x 0.0)))
 (let (($x958 (>= tbl4_kid_1_kid_0_hight 0.0)))
 (let (($x957 (>= tbl4_kid_1_kid_0_width 0.0)))
 (let (($x956 (>= tbl4_kid_1_kid_0_y 0.0)))
 (let (($x955 (>= tbl4_kid_1_kid_0_x 0.0)))
 (let (($x954 (or $x858 (= tbl4_kid_0_kid_2_hight 30.0))))
 (let (($x952 (or $x858 (= tbl4_kid_0_kid_0_hight 30.0))))
 (let ((?x943 (- (- tbl4_kid_0_kid_2_y tbl4_kid_0_kid_1_y) tbl4_kid_0_kid_1_hight)))
 (let (($x949 (or $x858 (= ?x943 10.0))))
 (let ((?x939 (- (- tbl4_kid_0_kid_1_y tbl4_kid_0_kid_0_y) tbl4_kid_0_kid_0_hight)))
 (let (($x947 (or $x858 (= ?x939 10.0))))
 (let (($x945 (or $x858 (>= ?x943 0.0))))
 (let (($x941 (or $x858 (>= ?x939 0.0))))
 (let ((?x935 (+ (- (- tbl4_kid_0_hight tbl4_kid_0_kid_2_y) tbl4_kid_0_kid_2_hight) tbl4_kid_0_y)))
 (let (($x937 (or $x858 (>= ?x935 20.0))))
 (let (($x932 (or $x858 (>= (- tbl4_kid_0_kid_2_y tbl4_kid_0_y) 20.0))))
 (let ((?x927 (- (- (+ tbl4_kid_0_x tbl4_kid_0_width) tbl4_kid_0_kid_2_x) tbl4_kid_0_kid_2_width)))
 (let (($x929 (or $x858 (>= ?x927 20.0))))
 (let (($x925 (or $x858 (>= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_2_x) 20.0))))
 (let ((?x921 (+ (- (- tbl4_kid_0_hight tbl4_kid_0_kid_1_y) tbl4_kid_0_kid_1_hight) tbl4_kid_0_y)))
 (let (($x923 (or $x858 (>= ?x921 20.0))))
 (let (($x918 (or $x858 (>= (- tbl4_kid_0_kid_1_y tbl4_kid_0_y) 20.0))))
 (let ((?x913 (- (- (+ tbl4_kid_0_x tbl4_kid_0_width) tbl4_kid_0_kid_1_x) tbl4_kid_0_kid_1_width)))
 (let (($x915 (or $x858 (>= ?x913 20.0))))
 (let (($x910 (or $x858 (>= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_1_x) 20.0))))
 (let ((?x906 (- (+ (- tbl4_kid_0_hight tbl4_kid_0_kid_0_y) tbl4_kid_0_y) tbl4_kid_0_kid_0_hight)))
 (let (($x908 (or $x858 (>= ?x906 20.0))))
 (let (($x903 (or $x858 (>= (- tbl4_kid_0_kid_0_y tbl4_kid_0_y) 20.0))))
 (let ((?x899 (- (+ (- tbl4_kid_0_x tbl4_kid_0_kid_0_width) tbl4_kid_0_width) tbl4_kid_0_kid_0_x)))
 (let (($x901 (or $x858 (>= ?x899 20.0))))
 (let (($x896 (or $x858 (>= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_0_x) 20.0))))
 (let (($x894 (= tbl4_kid_0_hight 350.0)))
 (let ((?x889 (+ (+ (- tbl4_kid_0_hight) tbl4_kid_0_kid_2_y) tbl4_kid_0_kid_2_hight)))
 (let (($x892 (or $x858 (= (- ?x889 tbl4_kid_0_y) (- 20.0)))))
 (let (($x886 (or $x858 (= (- tbl4_kid_0_kid_0_y tbl4_kid_0_y) 20.0))))
 (let ((?x881 (+ (+ (- (- tbl4_kid_0_x) tbl4_kid_0_width) tbl4_kid_0_kid_2_x) tbl4_kid_0_kid_2_width)))
 (let (($x883 (or $x858 (= ?x881 (- 20.0)))))
 (let ((?x877 (+ (+ (- (- tbl4_kid_0_x) tbl4_kid_0_width) tbl4_kid_0_kid_1_x) tbl4_kid_0_kid_1_width)))
 (let (($x879 (or $x858 (= ?x877 (- 20.0)))))
 (let ((?x871 (+ (- (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_0_width) tbl4_kid_0_width) tbl4_kid_0_kid_0_x)))
 (let (($x874 (or $x858 (= ?x871 (- 20.0)))))
 (let (($x868 (or $x858 (= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_2_x) 20.0))))
 (let (($x865 (or $x858 (= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_1_x) 20.0))))
 (let (($x862 (or $x858 (= (+ (- tbl4_kid_0_x) tbl4_kid_0_kid_0_x) 20.0))))
 (let (($x857 (>= tbl4_kid_0_kid_2_hight 0.0)))
 (let (($x856 (>= tbl4_kid_0_kid_2_width 0.0)))
 (let (($x855 (>= tbl4_kid_0_kid_2_y 0.0)))
 (let (($x854 (>= tbl4_kid_0_kid_2_x 0.0)))
 (let (($x853 (>= tbl4_kid_0_kid_1_hight 0.0)))
 (let (($x852 (>= tbl4_kid_0_kid_1_width 0.0)))
 (let (($x851 (>= tbl4_kid_0_kid_1_y 0.0)))
 (let (($x850 (>= tbl4_kid_0_kid_1_x 0.0)))
 (let (($x849 (>= tbl4_kid_0_kid_0_hight 0.0)))
 (let (($x848 (>= tbl4_kid_0_kid_0_width 0.0)))
 (let (($x847 (>= tbl4_kid_0_kid_0_y 0.0)))
 (let (($x846 (>= tbl4_kid_0_kid_0_x 0.0)))
 (let (($x845 (or $x652 $x844)))
 (let (($x842 (or $x652 $x841)))
 (let (($x838 (or $x652 $x837)))
 (let (($x834 (or $x652 (= (- tbl4_kid_0_hight tbl4_kid_4_hight) 0.0))))
 (let (($x830 (= (- (+ (- (- 10.0) tbl4_kid_0_hight) tbl4_kid_4_y) tbl4_kid_0_y) 0.0)))
 (let (($x831 (or $x652 $x830)))
 (let (($x825 (= (- (+ (- (- 10.0) tbl4_kid_2_width) tbl4_kid_3_x) tbl4_kid_2_x) 0.0)))
 (let (($x826 (or $x652 $x825)))
 (let (($x821 (or $x652 $x820)))
 (let (($x816 (or $x652 $x815)))
 (let (($x811 (or $x652 (= (+ (- tbl4_kid_7_width) tbl4_kid_3_width) 0.0))))
 (let (($x807 (or $x652 (= (- tbl4_kid_3_x tbl4_kid_7_x) 0.0))))
 (let (($x804 (or $x652 (= (- tbl4_kid_2_width tbl4_kid_6_width) 0.0))))
 (let (($x801 (or $x652 (= (+ (- tbl4_kid_6_x) tbl4_kid_2_x) 0.0))))
 (let (($x797 (or $x652 (= (- tbl4_kid_1_width tbl4_kid_5_width) 0.0))))
 (let (($x794 (or $x652 (= (- tbl4_kid_1_x tbl4_kid_5_x) 0.0))))
 (let (($x791 (or $x652 (= (- tbl4_kid_0_width tbl4_kid_4_width) 0.0))))
 (let (($x788 (or $x652 (= (- tbl4_kid_0_x tbl4_kid_4_x) 0.0))))
 (let (($x785 (or $x652 (= (+ (- tbl4_kid_7_hight) tbl4_kid_4_hight) 0.0))))
 (let (($x781 (or $x652 (= (- tbl4_kid_4_y tbl4_kid_7_y) 0.0))))
 (let (($x778 (or $x652 (= (+ (- tbl4_kid_6_hight) tbl4_kid_4_hight) 0.0))))
 (let (($x774 (or $x652 (= (- tbl4_kid_4_y tbl4_kid_6_y) 0.0))))
 (let (($x771 (or $x652 (= (+ (- tbl4_kid_5_hight) tbl4_kid_4_hight) 0.0))))
 (let (($x767 (or $x652 (= (+ (- tbl4_kid_5_y) tbl4_kid_4_y) 0.0))))
 (let (($x763 (or $x652 $x762)))
 (let (($x760 (or $x652 (= (+ (- tbl4_kid_3_y) tbl4_kid_0_y) 0.0))))
 (let (($x756 (or $x652 $x755)))
 (let (($x753 (or $x652 $x752)))
 (let (($x749 (or $x652 $x748)))
 (let (($x746 (or $x652 $x745)))
 (let (($x742 (= (+ (- (- tbl4_kid_7_hight tbl4_y) tbl4_hight) tbl4_kid_7_y) (- 10.0))))
 (let (($x743 (or $x652 $x742)))
 (let (($x737 (= (+ (- (- tbl4_kid_7_width tbl4_x) tbl4_width) tbl4_kid_7_x) (- 10.0))))
 (let (($x738 (or $x652 $x737)))
 (let (($x733 (or $x652 (= (+ (- tbl4_y) tbl4_kid_0_y) 10.0))))
 (let (($x729 (or $x652 (= (- tbl4_kid_0_x tbl4_x) 10.0))))
 (let (($x726 (or $x652 (> tbl4_kid_0_width 250.0))))
 (let (($x723 (>= tbl4_kid_7_hight 0.0)))
 (let (($x722 (>= tbl4_kid_7_width 0.0)))
 (let (($x721 (>= tbl4_kid_7_y 0.0)))
 (let (($x720 (>= tbl4_kid_7_x 0.0)))
 (let (($x719 (>= tbl4_kid_6_hight 0.0)))
 (let (($x718 (>= tbl4_kid_6_width 0.0)))
 (let (($x717 (>= tbl4_kid_6_y 0.0)))
 (let (($x716 (>= tbl4_kid_6_x 0.0)))
 (let (($x715 (>= tbl4_kid_5_hight 0.0)))
 (let (($x714 (>= tbl4_kid_5_width 0.0)))
 (let (($x713 (>= tbl4_kid_5_y 0.0)))
 (let (($x712 (>= tbl4_kid_5_x 0.0)))
 (let (($x711 (>= tbl4_kid_4_hight 0.0)))
 (let (($x710 (>= tbl4_kid_4_width 0.0)))
 (let (($x709 (>= tbl4_kid_4_y 0.0)))
 (let (($x708 (>= tbl4_kid_4_x 0.0)))
 (let (($x707 (>= tbl4_kid_3_hight 0.0)))
 (let (($x706 (>= tbl4_kid_3_width 0.0)))
 (let (($x705 (>= tbl4_kid_3_y 0.0)))
 (let (($x704 (>= tbl4_kid_3_x 0.0)))
 (let (($x703 (>= tbl4_kid_2_hight 0.0)))
 (let (($x702 (>= tbl4_kid_2_width 0.0)))
 (let (($x701 (>= tbl4_kid_2_y 0.0)))
 (let (($x700 (>= tbl4_kid_2_x 0.0)))
 (let (($x699 (>= tbl4_kid_1_hight 0.0)))
 (let (($x698 (>= tbl4_kid_1_width 0.0)))
 (let (($x697 (>= tbl4_kid_1_y 0.0)))
 (let (($x696 (>= tbl4_kid_1_x 0.0)))
 (let (($x695 (>= tbl4_kid_0_hight 0.0)))
 (let (($x694 (>= tbl4_kid_0_width 0.0)))
 (let (($x693 (>= tbl4_kid_0_y 0.0)))
 (let (($x692 (>= tbl4_kid_0_x 0.0)))
 (let ((?x690 (+ (+ (- (- main_body_x) main_body_width) tbl_holder_x) tbl_holder_width)))
 (let (($x691 (= ?x690 0.0)))
 (let ((?x296 (- main_body_x)))
 (let ((?x583 (+ ?x296 tbl_holder_x)))
 (let (($x687 (= ?x583 0.0)))
 (let (($x686 (or $x652 $x667)))
 (let (($x685 (or tbl4_feasible tbl3_feasible)))
 (let (($x683 (= (+ (- (- tbl3_hight tbl_holder_y) tbl_holder_hight) tbl3_y) 0.0)))
 (let (($x684 (or $x667 $x683)))
 (let (($x679 (or $x667 (= (+ (- tbl_holder_y) tbl3_y) 0.0))))
 (let (($x674 (= (- (- (+ tbl3_x tbl3_width) tbl_holder_x) tbl_holder_width) 0.0)))
 (let (($x675 (or $x667 $x674)))
 (let (($x670 (or $x667 (= (- tbl3_x tbl_holder_x) 0.0))))
 (let (($x665 (= (- (+ (- tbl4_y tbl_holder_y) tbl4_hight) tbl_holder_hight) 0.0)))
 (let (($x666 (or $x652 $x665)))
 (let (($x662 (or $x652 (= (- tbl4_y tbl_holder_y) 0.0))))
 (let (($x658 (= (- (+ (- tbl4_x tbl_holder_x) tbl4_width) tbl_holder_width) 0.0)))
 (let (($x659 (or $x652 $x658)))
 (let (($x655 (or $x652 (= (- tbl4_x tbl_holder_x) 0.0))))
 (let (($x651 (>= tbl3_hight 0.0)))
 (let (($x650 (>= tbl3_width 0.0)))
 (let (($x649 (>= tbl3_y 0.0)))
 (let (($x648 (>= tbl3_x 0.0)))
 (let (($x647 (>= tbl4_hight 0.0)))
 (let (($x646 (>= tbl4_width 0.0)))
 (let (($x645 (>= tbl4_y 0.0)))
 (let (($x644 (>= tbl4_x 0.0)))
 (let ((?x642 (+ (+ (- (* (- 2.0) main_body_x) main_body_width) (* 2.0 shop_x)) shop_width)))
 (let (($x643 (= ?x642 0.0)))
 (let (($x636 (= (+ (- 50.0) shop_hight) 0.0)))
 (let (($x634 (= (+ (- 200.0) shop_width) 0.0)))
 (let ((?x565 (- alexa_y main_body_y)))
 (let (($x631 (= ?x565 10.0)))
 (let ((?x628 (* 2.0 alexa_x)))
 (let ((?x629 (+ (- (- alexa_width (* 2.0 main_body_x)) main_body_width) ?x628)))
 (let (($x630 (= ?x629 0.0)))
 (let (($x625 (= (+ (- 150.0) alexa_hight) 0.0)))
 (let (($x622 (= (+ (- 300.0) alexa_width) 0.0)))
 (let (($x612 (> back_ground_width 1200.0)))
 (let (($x619 (or $x612 (= (+ (- main_body_width) back_ground_width) 0.0))))
 (let (($x614 (= main_body_width 1200.0)))
 (let (($x615 (or (not $x612) $x614)))
 (let ((?x608 (+ (- (* 2.0 main_body_x) (* 2.0 back_ground_x)) main_body_width)))
 (let (($x610 (= (- ?x608 back_ground_width) 0.0)))
 (let ((?x599 (- (+ (- shop_y) tbl_holder_y) shop_hight)))
 (let (($x603 (= ?x599 20.0)))
 (let ((?x595 (- (- shop_y alexa_y) alexa_hight)))
 (let (($x602 (= ?x595 20.0)))
 (let (($x600 (>= ?x599 0.0)))
 (let (($x596 (>= ?x595 0.0)))
 (let ((?x592 (+ (- (- main_body_hight tbl_holder_y) tbl_holder_hight) main_body_y)))
 (let (($x593 (>= ?x592 0.0)))
 (let (($x589 (>= (- tbl_holder_y main_body_y) 0.0)))
 (let ((?x586 (- (- (+ main_body_x main_body_width) tbl_holder_x) tbl_holder_width)))
 (let (($x587 (>= ?x586 0.0)))
 (let (($x584 (>= ?x583 0.0)))
 (let (($x582 (>= (+ (- (- main_body_hight shop_y) shop_hight) main_body_y) 0.0)))
 (let (($x578 (>= (- shop_y main_body_y) 0.0)))
 (let (($x576 (>= (- (- (+ main_body_x main_body_width) shop_x) shop_width) 0.0)))
 (let (($x572 (>= (+ ?x296 shop_x) 0.0)))
 (let (($x570 (>= (+ (- (- main_body_hight alexa_y) alexa_hight) main_body_y) 0.0)))
 (let (($x566 (>= ?x565 0.0)))
 (let (($x564 (>= (- (+ (+ (- alexa_width) main_body_x) main_body_width) alexa_x) 0.0)))
 (let (($x559 (>= (+ ?x296 alexa_x) 0.0)))
 (let (($x557 (>= tbl_holder_hight 0.0)))
 (let (($x556 (>= tbl_holder_width 0.0)))
 (let (($x555 (>= tbl_holder_y 0.0)))
 (let (($x554 (>= tbl_holder_x 0.0)))
 (let (($x553 (>= shop_hight 0.0)))
 (let (($x552 (>= shop_width 0.0)))
 (let (($x551 (>= shop_y 0.0)))
 (let (($x550 (>= shop_x 0.0)))
 (let (($x549 (>= alexa_hight 0.0)))
 (let (($x548 (>= alexa_width 0.0)))
 (let (($x547 (>= alexa_y 0.0)))
 (let (($x546 (>= alexa_x 0.0)))
 (let (($x545 (= (- (- (+ (- 100.0) accounts_x) search_go_x) search_go_width) 0.0)))
 (let ((?x407 (- (+ (- search_bar_x) search_go_x) search_bar_width)))
 (let (($x541 (= ?x407 0.0)))
 (let (($x540 (= (- (+ (- (- 100.0) icon_width) search_bar_x) icon_x) 0.0)))
 (let (($x535 (= (+ (- 50.0) search_go_width) 0.0)))
 (let (($x532 (= your_account_width 100.0)))
 (let (($x530 (= (+ (- Basket_width) your_account_width) 0.0)))
 (let (($x527 (= (- your_account_width Help_width) 0.0)))
 (let ((?x502 (- (+ (- Help_x) Basket_x) Help_width)))
 (let (($x525 (= ?x502 10.0)))
 (let ((?x499 (- (- Help_x your_account_x) your_account_width)))
 (let (($x524 (= ?x499 10.0)))
 (let (($x523 (= (+ (+ (- (- accounts_y) accounts_hight) Basket_y) Basket_hight) (- 10.0))))
 (let (($x519 (= (+ (- (+ (- accounts_y) Help_hight) accounts_hight) Help_y) (- 10.0))))
 (let ((?x514 (+ (- (+ (- accounts_y) your_account_hight) accounts_hight) your_account_y)))
 (let (($x515 (= ?x514 (- 10.0))))
 (let ((?x397 (- accounts_y)))
 (let ((?x492 (+ ?x397 Basket_y)))
 (let (($x511 (= ?x492 10.0)))
 (let ((?x479 (+ ?x397 Help_y)))
 (let (($x510 (= ?x479 10.0)))
 (let ((?x466 (+ ?x397 your_account_y)))
 (let (($x509 (= ?x466 10.0)))
 (let (($x508 (= (- (- (+ Basket_x Basket_width) accounts_x) accounts_width) (- 10.0))))
 (let ((?x459 (- your_account_x accounts_x)))
 (let (($x504 (= ?x459 10.0)))
 (let (($x503 (>= ?x502 0.0)))
 (let (($x500 (>= ?x499 0.0)))
 (let (($x497 (>= (- (- (+ accounts_y accounts_hight) Basket_y) Basket_hight) 0.0)))
 (let (($x493 (>= ?x492 0.0)))
 (let (($x491 (>= (+ (+ (- (- Basket_x) Basket_width) accounts_x) accounts_width) 0.0)))
 (let (($x486 (>= (- Basket_x accounts_x) 0.0)))
 (let (($x484 (>= (- (+ (- accounts_y Help_hight) accounts_hight) Help_y) 0.0)))
 (let (($x480 (>= ?x479 0.0)))
 (let (($x478 (>= (+ (- (+ (- Help_x) accounts_x) Help_width) accounts_width) 0.0)))
 (let (($x473 (>= (- Help_x accounts_x) 0.0)))
 (let ((?x470 (- (+ (- accounts_y your_account_hight) accounts_hight) your_account_y)))
 (let (($x471 (>= ?x470 0.0)))
 (let (($x467 (>= ?x466 0.0)))
 (let ((?x464 (+ (- (+ (- your_account_x) accounts_x) your_account_width) accounts_width)))
 (let (($x465 (>= ?x464 0.0)))
 (let (($x460 (>= ?x459 0.0)))
 (let (($x458 (>= Basket_hight 0.0)))
 (let (($x457 (>= Basket_width 0.0)))
 (let (($x456 (>= Basket_y 0.0)))
 (let (($x455 (>= Basket_x 0.0)))
 (let (($x454 (>= Help_hight 0.0)))
 (let (($x453 (>= Help_width 0.0)))
 (let (($x452 (>= Help_y 0.0)))
 (let (($x451 (>= Help_x 0.0)))
 (let (($x450 (>= your_account_hight 0.0)))
 (let (($x449 (>= your_account_width 0.0)))
 (let (($x448 (>= your_account_y 0.0)))
 (let (($x447 (>= your_account_x 0.0)))
 (let (($x446 (= (+ (- 80.0) icon_width) 0.0)))
 (let (($x443 (= search_hight 80.0)))
 (let (($x441 (= (- (+ (- accounts_y search_hight) accounts_hight) search_y) (- 10.0))))
 (let ((?x436 (- (+ (+ (- search_hight) search_go_y) search_go_hight) search_y)))
 (let (($x437 (= ?x436 (- 10.0))))
 (let ((?x432 (- (+ (+ (- search_hight) search_bar_y) search_bar_hight) search_y)))
 (let (($x433 (= ?x432 (- 10.0))))
 (let (($x429 (= (- (+ (+ (- search_hight) icon_y) icon_hight) search_y) (- 10.0))))
 (let ((?x395 (- accounts_y search_y)))
 (let (($x425 (= ?x395 10.0)))
 (let ((?x383 (- search_go_y search_y)))
 (let (($x424 (= ?x383 10.0)))
 (let ((?x372 (- search_bar_y search_y)))
 (let (($x423 (= ?x372 10.0)))
 (let ((?x360 (- icon_y search_y)))
 (let (($x422 (= ?x360 10.0)))
 (let (($x421 (= (+ (- (+ (- search_x) accounts_x) search_width) accounts_width) (- 10.0))))
 (let ((?x282 (- search_x)))
 (let ((?x353 (+ ?x282 icon_x)))
 (let (($x417 (= ?x353 10.0)))
 (let (($x415 (= (- (+ (- search_x back_ground_x) search_width) back_ground_width) 0.0)))
 (let ((?x280 (- search_x back_ground_x)))
 (let (($x412 (= ?x280 0.0)))
 (let (($x411 (>= (- (- accounts_x search_go_x) search_go_width) 0.0)))
 (let (($x408 (>= ?x407 0.0)))
 (let (($x404 (>= (- (+ (- icon_width) search_bar_x) icon_x) 0.0)))
 (let (($x401 (>= (+ (- (+ ?x397 search_hight) accounts_hight) search_y) 0.0)))
 (let (($x396 (>= ?x395 0.0)))
 (let (($x394 (>= (- (+ (- search_x accounts_x) search_width) accounts_width) 0.0)))
 (let ((?x389 (+ ?x282 accounts_x)))
 (let (($x390 (>= ?x389 0.0)))
 (let (($x388 (>= (+ (- (- search_hight search_go_y) search_go_hight) search_y) 0.0)))
 (let (($x384 (>= ?x383 0.0)))
 (let (($x382 (>= (- (- (+ search_x search_width) search_go_x) search_go_width) 0.0)))
 (let (($x379 (>= (+ ?x282 search_go_x) 0.0)))
 (let (($x377 (>= (+ (- (- search_hight search_bar_y) search_bar_hight) search_y) 0.0)))
 (let (($x373 (>= ?x372 0.0)))
 (let (($x371 (>= (- (- (+ search_x search_width) search_bar_x) search_bar_width) 0.0)))
 (let (($x367 (>= (+ ?x282 search_bar_x) 0.0)))
 (let (($x365 (>= (+ (- (- search_hight icon_y) icon_hight) search_y) 0.0)))
 (let (($x361 (>= ?x360 0.0)))
 (let (($x359 (>= (- (+ (+ (- icon_width) search_x) search_width) icon_x) 0.0)))
 (let (($x354 (>= ?x353 0.0)))
 (let (($x352 (>= accounts_hight 0.0)))
 (let (($x351 (>= accounts_width 0.0)))
 (let (($x350 (>= accounts_y 0.0)))
 (let (($x349 (>= accounts_x 0.0)))
 (let (($x348 (>= search_go_hight 0.0)))
 (let (($x347 (>= search_go_width 0.0)))
 (let (($x346 (>= search_go_y 0.0)))
 (let (($x345 (>= search_go_x 0.0)))
 (let (($x344 (>= search_bar_hight 0.0)))
 (let (($x343 (>= search_bar_width 0.0)))
 (let (($x342 (>= search_bar_y 0.0)))
 (let (($x341 (>= search_bar_x 0.0)))
 (let (($x340 (>= icon_hight 0.0)))
 (let (($x339 (>= icon_width 0.0)))
 (let (($x338 (>= icon_y 0.0)))
 (let (($x337 (>= icon_x 0.0)))
 (let (($x336 (= (+ (- (+ (- BC_width) back_ground_x) BC_x) back_ground_width) 0.0)))
 (let (($x331 (= (- back_ground_x BC_x) 0.0)))
 (let ((?x326 (- (+ (- main_body_hight) bottom_y) main_body_y)))
 (let (($x329 (= ?x326 0.0)))
 (let ((?x322 (+ (- (- search_hight) search_y) main_body_y)))
 (let (($x328 (= ?x322 0.0)))
 (let (($x327 (>= ?x326 0.0)))
 (let (($x323 (>= ?x322 0.0)))
 (let (($x319 (>= (- (- (+ back_ground_y back_ground_hight) bottom_y) bottom_hight) 0.0)))
 (let (($x315 (>= (+ (- back_ground_y) bottom_y) 0.0)))
 (let ((?x312 (+ (+ (- (- bottom_x) bottom_width) back_ground_x) back_ground_width)))
 (let (($x313 (>= ?x312 0.0)))
 (let (($x308 (>= ?x307 0.0)))
 (let ((?x305 (- (+ (- back_ground_y main_body_hight) back_ground_hight) main_body_y)))
 (let (($x306 (>= ?x305 0.0)))
 (let (($x302 (>= (+ (- back_ground_y) main_body_y) 0.0)))
 (let (($x300 (>= (+ (- (+ ?x296 back_ground_x) main_body_width) back_ground_width) 0.0)))
 (let (($x295 (>= (- main_body_x back_ground_x) 0.0)))
 (let (($x293 (>= (- (+ (- back_ground_y search_hight) back_ground_hight) search_y) 0.0)))
 (let (($x289 (>= (+ (- back_ground_y) search_y) 0.0)))
 (let (($x286 (>= (+ (- (+ ?x282 back_ground_x) search_width) back_ground_width) 0.0)))
 (let (($x281 (>= ?x280 0.0)))
 (let (($x279 (>= bottom_hight 0.0)))
 (let (($x278 (>= bottom_width 0.0)))
 (let (($x277 (>= bottom_y 0.0)))
 (let (($x276 (>= bottom_x 0.0)))
 (let (($x275 (>= main_body_hight 0.0)))
 (let (($x274 (>= main_body_width 0.0)))
 (let (($x273 (>= main_body_y 0.0)))
 (let (($x272 (>= main_body_x 0.0)))
 (let (($x271 (>= search_hight 0.0)))
 (let (($x270 (>= search_width 0.0)))
 (let (($x269 (>= search_y 0.0)))
 (let (($x268 (>= search_x 0.0)))
 (let (($x267 (>= back_ground_hight 0.0)))
 (let (($x266 (>= back_ground_width 0.0)))
 (let (($x265 (>= back_ground_y 0.0)))
 (let (($x264 (>= back_ground_x 0.0)))
 (let (($x263 (= BC_y 0.0)))
 (let (($x262 (= BC_x 0.0)))
 (let (($x261 (<= BC_width 4000.0)))
 (let (($x259 (>= BC_hight 0.0)))
 (let (($x258 (>= BC_width 0.0)))
 (let (($x257 (>= BC_y 0.0)))
 (let (($x256 (>= BC_x 0.0)))
 (and $x256 $x257 $x258 $x259 $x261 $x262 $x263 BC_feasible $x264 $x265 $x266 $x267 $x268 $x269 $x270 $x271 $x272 $x273 $x274 $x275 $x276 $x277 $x278 $x279 $x281 $x286 $x289 $x293 $x295 $x300 $x302 $x306 $x308 $x313 $x315 $x319 $x323 $x327 $x328 $x329 $x331 $x336 $x337 $x338 $x339 $x340 $x341 $x342 $x343 $x344 $x345 $x346 $x347 $x348 $x349 $x350 $x351 $x352 $x354 $x359 $x361 $x365 $x367 $x371 $x373 $x377 $x379 $x382 $x384 $x388 $x390 $x394 $x396 $x401 $x404 $x408 $x411 $x412 $x415 $x417 $x421 $x422 $x423 $x424 $x425 $x429 $x433 $x437 $x441 $x443 $x446 $x447 $x448 $x449 $x450 $x451 $x452 $x453 $x454 $x455 $x456 $x457 $x458 $x460 $x465 $x467 $x471 $x473 $x478 $x480 $x484 $x486 $x491 $x493 $x497 $x500 $x503 $x504 $x508 $x509 $x510 $x511 $x515 $x519 $x523 $x524 $x525 $x527 $x530 $x532 $x535 $x540 $x541 $x545 $x546 $x547 $x548 $x549 $x550 $x551 $x552 $x553 $x554 $x555 $x556 $x557 $x559 $x564 $x566 $x570 $x572 $x576 $x578 $x582 $x584 $x587 $x589 $x593 $x596 $x600 $x602 $x603 $x610 $x615 $x619 $x622 $x625 $x630 $x631 $x634 $x636 $x643 $x644 $x645 $x646 $x647 $x648 $x649 $x650 $x651 $x655 $x659 $x662 $x666 $x670 $x675 $x679 $x684 $x685 $x686 $x687 $x691 $x692 $x693 $x694 $x695 $x696 $x697 $x698 $x699 $x700 $x701 $x702 $x703 $x704 $x705 $x706 $x707 $x708 $x709 $x710 $x711 $x712 $x713 $x714 $x715 $x716 $x717 $x718 $x719 $x720 $x721 $x722 $x723 $x726 $x729 $x733 $x738 $x743 $x746 $x749 $x753 $x756 $x760 $x763 $x767 $x771 $x774 $x778 $x781 $x785 $x788 $x791 $x794 $x797 $x801 $x804 $x807 $x811 $x816 $x821 $x826 $x831 $x834 $x838 $x842 $x845 $x846 $x847 $x848 $x849 $x850 $x851 $x852 $x853 $x854 $x855 $x856 $x857 $x862 $x865 $x868 $x874 $x879 $x883 $x886 $x892 $x894 $x896 $x901 $x903 $x908 $x910 $x915 $x918 $x923 $x925 $x929 $x932 $x937 $x941 $x945 $x947 $x949 $x952 $x954 $x955 $x956 $x957 $x958 $x959 $x960 $x961 $x962 $x963 $x964 $x965 $x966 $x971 $x974 $x977 $x982 $x986 $x990 $x993 $x998 $x999 $x1001 $x1006 $x1008 $x1014 $x1016 $x1020 $x1023 $x1029 $x1031 $x1036 $x1040 $x1046 $x1050 $x1053 $x1055 $x1057 $x1059 $x1061 $x1062 $x1063 $x1064 $x1065 $x1066 $x1067 $x1068 $x1069 $x1070 $x1071 $x1072 $x1073 $x1078 $x1081 $x1084 $x1089 $x1094 $x1099 $x1102 $x1107 $x1108 $x1110 $x1115 $x1117 $x1123 $x1125 $x1130 $x1133 $x1138 $x1140 $x1146 $x1148 $x1154 $x1158 $x1162 $x1164 $x1166 $x1168 $x1170 $x1171 $x1172 $x1173 $x1174 $x1175 $x1176 $x1177 $x1178 $x1179 $x1180 $x1181 $x1182 $x1186 $x1189 $x1192 $x1196 $x1200 $x1205 $x1208 $x1213 $x1214 $x1216 $x1222 $x1224 $x1230 $x1232 $x1238 $x1241 $x1247 $x1249 $x1255 $x1258 $x1264 $x1268 $x1272 $x1274 $x1276 $x1278 $x1280 $x1281 $x1282 $x1283 $x1284 $x1285 $x1286 $x1287 $x1288 $x1289 $x1290 $x1291 $x1292 $x1296 $x1300 $x1303 $x1308 $x1313 $x1318 $x1322 $x1327 $x1328 $x1330 $x1336 $x1338 $x1343 $x1345 $x1351 $x1354 $x1358 $x1360 $x1366 $x1369 $x1373 $x1377 $x1382 $x1384 $x1386 $x1388 $x1390 $x1391 $x1392 $x1393 $x1394 $x1395 $x1396 $x1397 $x1398 $x1399 $x1400 $x1401 $x1402 $x1407 $x1410 $x1413 $x1418 $x1422 $x1426 $x1429 $x1434 $x1435 $x1437 $x1442 $x1444 $x1449 $x1451 $x1456 $x1459 $x1464 $x1466 $x1472 $x1475 $x1479 $x1483 $x1488 $x1490 $x1492 $x1494 $x1496 $x1497 $x1498 $x1499 $x1500 $x1501 $x1502 $x1503 $x1504 $x1505 $x1506 $x1507 $x1508 $x1512 $x1515 $x1518 $x1522 $x1526 $x1531 $x1535 $x1540 $x1541 $x1543 $x1548 $x1550 $x1555 $x1557 $x1563 $x1566 $x1571 $x1573 $x1579 $x1582 $x1587 $x1592 $x1596 $x1598 $x1600 $x1602 $x1604 $x1605 $x1606 $x1607 $x1608 $x1609 $x1610 $x1611 $x1612 $x1613 $x1614 $x1615 $x1616 $x1620 $x1623 $x1626 $x1631 $x1636 $x1641 $x1644 $x1649 $x1650 $x1652 $x1658 $x1660 $x1665 $x1667 $x1672 $x1675 $x1680 $x1682 $x1687 $x1690 $x1695 $x1699 $x1703 $x1705 $x1707 $x1709 $x1711 $x1714 $x1717 $x1723 $x1728 $x1729 $x1730 $x1731 $x1732 $x1735 $x1738 $x1741 $x1744 $x1747 $x1748 $x1751 $x1754 $x1757 $x1760 $x1761 $x1762 $x1766 $x1767 $x1768 $x1769 $x1770 $x1774 $x1776 $x1777 $x1778 $x1779 $x1780 $x1786 $x1792 $x1794 $x1796 back_ground_feasible search_feasible main_body_feasible bottom_feasible icon_feasible search_bar_feasible search_go_feasible accounts_feasible your_account_feasible Help_feasible Basket_feasible alexa_feasible shop_feasible tbl_holder_feasible $x1797 $x1798 $x1799 $x1800 $x1801 $x1802 $x1803 $x1804 $x1805 $x1806 $x1807 $x1808 $x1809 $x1810 $x1811 $x1812 $x1813 $x1814 $x1815 $x1816 $x1817 $x1818 $x1819 $x1820 $x1821 $x1822 $x1823 $x1824 $x1826 $x1827 $x1829 $x1830 $x1832 $x1833 $x1835 $x1836 $x1838 $x1839 $x1841 $x1842 $x1844 $x1845 $x1847 $x1848 $x1850 $x1851 $x1853 $x1854 $x1856 $x1857 $x1859 $x1860 $x1862 $x1863 $x1865 $x1866 $x1868 $x1869 $x1871 $x1872 $x1874 $x1875 $x1877 $x1878 $x1880 $x1881 $x1883 $x1884 $x1886 $x1887 $x1889 $x1890 $x1892 $x1893 $x1895 $x1896 icon2_feasible))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

